460-4016/02 – Modelování a verifikace (MaV)
| Garantující katedra | Katedra informatiky | Kredity | 4 |
| Garant předmětu | Ing. Martin Kot, Ph.D. | Garant verze předmětu | Ing. Martin Kot, Ph.D. |
| Úroveň studia | pregraduální nebo graduální | | |
| | Jazyk výuky | angličtina |
| Rok zavedení | 2015/2016 | Rok zrušení | |
| Určeno pro fakulty | FEI | Určeno pro typy studia | navazující magisterské |
Cíle předmětu vyjádřené dosaženými dovednostmi a kompetencemi
Student po úspěšném absolvování předmětu:
- zná základní pojmy v oblasti modelování kalkulem komunikujících
systémů (CCS) a časovými automaty,
- rozumí základní teorii potřebné k modelování a ověřování systémů,
včetně bisimulační ekvivalence,
- umí vyjadřovat běžně testované vlastnosti systémů formulemi
temporálních logik,
- zvládá práci s vybranými modelovacími a verifikačními softwarovými
nástroji,
- je schopen analyzovat, modelovat a ověřovat malé praktické systémy
(jako jsou např. komunikační protokoly).
Vyučovací metody
Přednášky
Cvičení (v učebně)
Anotace
Problém korektnosti, tedy problém ověření (neboli verifikace), že daný počítačový (hardwarový a/nebo softwarový) systém má skutečně vlastnosti, které jsou požadovány jeho specifikací, patří mezi fundamentální praktické i teoretické problémy v oblasti informatiky. Neustálý rozvoj informačních technologií vede k vytváření stále složitějších systémů, a tak nejen výzkumná, ale i průmyslová praxe se neobejde bez solidně vybudovaných verifikačních postupů. Jako jedna třída prakticky úspěšných metod se v devadesátých letech dvacátého století etablovala automatická verifikace zahrnující i tzv. `ověření modelu' (model checking); testovaná vlastnost systému se přitom vyjádří např. v jednoduché temporální logice a ověřuje se (polo)automatickými metodami na modelu systému. Účelem kursu je vysvětlení základních principů této (automatické) verifikace a zároveň demonstrace této verifikace na modelech konkrétních praktických problémů, pro něž jsou vhodné volně dostupné softwarové verifikační nástroje.
Povinná literatura:
1. Luca Aceto, Anna Ingólfsdóttir, Kim G. Larsen and Jiří Srba: Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, August 2007.
2. Gerd Behrmann, Alexandre David, Kim G. Larsen: A Tutorial on Uppaal 4.0. Dostupné online na https://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf [14.4.2021]
Doporučená literatura:
1. Gerard J. Holzmann: The SPIN MODEL CHECKER: Primer and Reference Manual. Addison-Wesley, 2003
2. Christel Baier, Joost-Pieter Katoen: Principles of Model Checking. MIT Press, 2008.
Forma způsobu ověření studijních výsledků a další požadavky na studenta
Řešení a diskuse písemně zadaných úloh pro jednotlivá cvičení.
Zpracování dvou miniprojektů s asistencí, zakončených vytvořením souborů sloužících jako vstup do verifikačních SW nástrojů.
Závěrečná zkouška (ústní s písemnou přípravou).
E-learning
Elektronické podklady k přednáškám, obsah cvičení, odkazy na softwarové nástroje a další informace jsou přístupné z webové stránky předmětu.
Další požadavky na studenta
Další požadavky na studenta nejsou kladeny.
Prerekvizity
Předmět nemá žádné prerekvizity.
Korekvizity
Předmět nemá žádné korekvizity.
Osnova předmětu
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í.
Podmínky absolvování předmětu
Výskyt ve studijních plánech
Výskyt ve speciálních blocích
Hodnocení Výuky
Předmět neobsahuje žádné hodnocení.