|
Vyučující
|
-
Jančar Petr, prof. RNDr. CSc.
|
|
Obsah předmětu
|
1. Úvod. Pojem reaktivních systémů, příklady. Přechodové systémy jako základní model. Neformální uvedení jazyka CCS (Kalkulus komunikujících systémů) pro popis (reaktivních) systémů. 2. Kompletní definice jazyka CCS (syntaxe a sémantika), příklady. CCS s proměnnými. 3. Behaviorální ekvivalence (tj. pojem ekvivalentního chování systémů). Ekvivalence podle množin běhů (trace equivalence). Bisimulační ekvivalence; bisimulační hry. 4. Vlastnosti silné bisimulační ekvivalence. Interní akce. Slabá bisimulační ekvivalence. Příklad (malý komunikační protokol). 5. Softwarový nástroj Concurrency Workbench, CWB (Edinburgh, UK). Modální logika HML (Henessy-Milner Logic); popis jednoduchých vlastností chování systému. 6. Další příklady v CWB. Korespondence bisimulační ekvivalence a HM-logiky. Význam abstraktního pojmu pevného bodu v úplných svazech pro definici sémantiky rekurzivních programů. 7. Výpočet bisimulační ekvivalenci jako pevného bodu. HM-logika s rekurzí; charakterizace pomocí her. 8. Vyřešení malého projektu: modelování protokolu s alternujícím bitem (alternating bit protocol) v jazyku CCS a verifikace v nástroji CWB. 9. Přechodové systémy s časem. Jazyk CCS s časem (timed CCS) a časované automaty (timed automata). 10. Časovaná a nečasovaná bisimulační ekvivalence. Konstrukce regionů (regions) u časovaných automatů. HM-logika s časem. 11. Softwarový nástroj UPPAAL (založený na časovaných automatech). Modelování, specifikace, simulace a verifikace v UPPAALu na praktických příkladech. 12. Vyřešení malého projektu: modelování a analýza `drbajících dívek' (gossiping girls) v nástroji UPPAAL. 13. Stručná informace o dalších oblastech verifikace. Shrnutí kursu, podrobné informace o formě a obsahu zkoušky.
|
|
Studijní aktivity a metody výuky
|
|
Přednášení, Laborování
|
|
Výstupy z učení
|
Studenti získají praktickou zkušenost s verifikací programů a seznámí se s příslušnými teoretickými základy.
1. Znalost Popsat a důkladně pochopit principy verifikace souběžných (distribuovaných) programů.
|
|
Předpoklady
|
nespecifikováno
|
|
Hodnoticí metody a kritéria
|
Ústní zkouška, Seminární práce
Aktivní účast v hodině. Plnění zadaných úkolů, speciálně dvou malých projektů. Složení ústní (příp. písemné) zkoušky.
|
|
Doporučená literatura
|
-
Volně dostupné tutoriály k verifikačním nástrojům (CWB, UPPAAL).
-
Aceto L., Ingólfsdóttir A., Larsen K.G., Srba J. (2007). Reactive Systems: Modelling, Specification and Verification. Cambridge University Press.
-
Baier C., Katoen J.-P. (2008). Principles of Model Checking. The MIT Press.
-
Clarke E.M., Henzinger T.A., Veith H., and Bloem R. (2018). Handbook of Model Checking. Springer.
-
Clarke M., Grumberg O. and Peled D. A. (2000). Model checking. The MIT Press.
-
Manna Z. (1981). Matematická teorie programů. SNTL Praha.
-
Peled D. (2001). Software Reliability Methods. Springer.
-
Schneider K. (2004). Verification of Reactive Systems: Formal Methods and Algorithms. Springer.
|