|
Vyučující
|
-
Jančar Petr, prof. RNDr. CSc.
|
|
Obsah předmětu
|
Předmět je zaměřen na hlubší pochopení formálních metod zejména v oblasti automatizované verifikace systémů. Zahrnuje např. tyto části: Logika a částečně automatizované dokazování teorémů. Modelování softwarových a hardwarových systémů. Formální specifikace, temporální logiky a automaty. Automatizovaná verifikace, ověřování modelu (model checking). Procesní algebry a ekvivalence. Softwarové verifikační nástroje.
|
|
Studijní aktivity a metody výuky
|
|
Dialogická (diskuze, rozhovor, brainstorming), Metody práce s textem (učebnicí, knihou)
|
|
Výstupy z učení
|
Studenti se seznámí se základními metodami pro rigorózní ověření požadovaného chování (softwarových či hardwarových) systémů a porozumí teoretickým základům těchto metod a možnostem jejich praktického nasazení.
1. Znalost Pochopení principů formálních metod verifikace systémů a jejich nasazení v praxi.
|
|
Předpoklady
|
nespecifikováno
|
|
Hodnoticí metody a kritéria
|
Ústní zkouška
Plnění zadaných úkolů. Složení zkoušky.
|
|
Doporučená literatura
|
-
Clarke E.M., Grumberg O., Peled D. (1999). Model Checking. MIT Press.
-
Clarke, E.M., Henzinger, Th.A., Veith, H., Bloem, R. (Eds). (2018). Handbook of Model Checking. Springer.
-
Manna Z. (1981). Matematická teorie programů. SNTL Praha.
-
Schneider K. (2004). Verification of Reactive Systems (Formal Methods and Algorithms). Springer.
|