Přednášky:
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. Modální logika HML (Henessy-Milner Logic); popis jednoduchých vlastností chování systému.
6. Význam abstraktního pojmu pevného bodu v úplných svazech pro definici sémantiky rekurzivních programů. Výpočet bisimulační ekvivalenci jako pevného bodu. HM-logika s rekurzí; charakterizace pomocí her. Korespondence bisimulační ekvivalence a HM-logiky.
7. Softwarový nástroj CAAL (Concurrency Workbench, Aalborg Edition).
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 CAAL.
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 zadaného úkolu v nástroji UPPAAL.
13. Stručná informace o dalších oblastech verifikace. Shrnutí kursu, podrobné informace o formě a obsahu zkoušky.
Cvičení:
1. Procvičení příkladů jednoduchých přechodových systémů a zápisů v CCS.
2. Příklady malých systémů popsaných v CCS. Neformální diskuse (ne)ekvivalence jejich chování.
3. Procvičení pojmu bisimulační ekvivalence formou bisimulačních her na malých přechodových systémech.
4. Důkazy ekvivalentního chování vzhledem k slabé bisimulační ekvivalenci - pro malé systémy s tužkou a papírem.
5. Vyjadřování jednoduchých vlastností v HM-logice.
6. Procvičení významu (sémantiky) rekurzivních programů pomocí výpočtu pevného bodu. Příklady HML-formulí s rekurzí.
7. Praktické uvedení softwarového nástroje CAAL. Příprava na první malý projekt (protokol s alternujícím bitem).
8. Dokončení projektu modelování a verifikace protokolu s alternujícím bitem (v nástroji CAAL).
9. Příklady modelů malých systémů s časem, popsaných v časovaném CCS a pomocí časovaných automatů.
10. Příklady ekvivalentních systémů z hlediska časované bisimulační ekvivalence. Výpočet regionů (regions) u časovaných automatů.
11. Praktické uvedení softwarového nástroje UPPAAL. Příprava na druhý malý projekt.
12. Dokončení projektu modelování a verifikace zadaného problému v nástroji UPPAAL.
13. Shrnutí vyřešených příkladů a miniprojektů a diskuse klíčových problémů (s ohledem na zkoušku).
Počítačové laboratoře:
Koná se v rámci výše uvedených cvičení.
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. Modální logika HML (Henessy-Milner Logic); popis jednoduchých vlastností chování systému.
6. Význam abstraktního pojmu pevného bodu v úplných svazech pro definici sémantiky rekurzivních programů. Výpočet bisimulační ekvivalenci jako pevného bodu. HM-logika s rekurzí; charakterizace pomocí her. Korespondence bisimulační ekvivalence a HM-logiky.
7. Softwarový nástroj CAAL (Concurrency Workbench, Aalborg Edition).
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 CAAL.
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 zadaného úkolu v nástroji UPPAAL.
13. Stručná informace o dalších oblastech verifikace. Shrnutí kursu, podrobné informace o formě a obsahu zkoušky.
Cvičení:
1. Procvičení příkladů jednoduchých přechodových systémů a zápisů v CCS.
2. Příklady malých systémů popsaných v CCS. Neformální diskuse (ne)ekvivalence jejich chování.
3. Procvičení pojmu bisimulační ekvivalence formou bisimulačních her na malých přechodových systémech.
4. Důkazy ekvivalentního chování vzhledem k slabé bisimulační ekvivalenci - pro malé systémy s tužkou a papírem.
5. Vyjadřování jednoduchých vlastností v HM-logice.
6. Procvičení významu (sémantiky) rekurzivních programů pomocí výpočtu pevného bodu. Příklady HML-formulí s rekurzí.
7. Praktické uvedení softwarového nástroje CAAL. Příprava na první malý projekt (protokol s alternujícím bitem).
8. Dokončení projektu modelování a verifikace protokolu s alternujícím bitem (v nástroji CAAL).
9. Příklady modelů malých systémů s časem, popsaných v časovaném CCS a pomocí časovaných automatů.
10. Příklady ekvivalentních systémů z hlediska časované bisimulační ekvivalence. Výpočet regionů (regions) u časovaných automatů.
11. Praktické uvedení softwarového nástroje UPPAAL. Příprava na druhý malý projekt.
12. Dokončení projektu modelování a verifikace zadaného problému v nástroji UPPAAL.
13. Shrnutí vyřešených příkladů a miniprojektů a diskuse klíčových problémů (s ohledem na zkoušku).
Počítačové laboratoře:
Koná se v rámci výše uvedených cvičení.