1. Úloha formálních specifikací a modelů v softwarovém inženýrství, jejich výhody a nevýhody.
2. Algebraické metody, vícedruhové algebry, iniciální modely.
3. Přepisovací systémy, OBJ3, Maude.
4. Modelově orientované metody.
5. Jazyk Z a vybrané nadstavby (Objective-Z).
6. Metoda VDM a její nadstavby (VDM++).
7. Úvod do jazyka Alloy.
8. Formální základy UML.
9. Specifikační jazyk OCL.
10. Petriho sítě a CPN.
11. Temporální logika. Dynamická logika.
12. Doménově specifické jazyky.
Role formálních specifikací a modelů v softwarovém inženýrství. Přehled vybraných metod a nástrojů pro formální popis architektury a chování systému. Ukázky jejich použití zejména ve fázích návrhu a validace.
Předpokládají se znalosti v rozsahu předmětu NSWI041 - Úvod do softwarového inženýrství.