Předmět Modelování a verifikace (MaV)

Na serveru studentino.cz naleznete nejrůznější studijní materiály: zápisky z přednášek nebo cvičení, vzorové testy, seminární práce, domácí úkoly a další z předmětu MaV - Modelování a verifikace, Vysoká škola báňská - Technická univerzita Ostrava (VŠB-TU).

Materiál	Typ	Datum	Počet stažení

Cíl

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).

Osnova

Přednášky: Ú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ů.Kompletní definice jazyka CCS (syntaxe a sémantika), příklady.CCS s proměnnými. 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.Vlastnosti silné bisimulační ekvivalence. Interní akce. Slabá bisimulační ekvivalence. Příklad (malý komunikační protokol).Softwarový nástroj Concurrency Workbench, CWB (Edinburgh, UK).Modální logika HML (Henessy-Milner Logic); popis jednoduchýchvlastností chování systému.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ů.Výpočet bisimulační ekvivalenci jako pevného bodu.HM-logika s rekurzí; charakterizace pomocí her.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. Přechodové systémy s časem.Jazyk CCS s časem (timed CCS) a časované automaty (timed automata).Časovaná a nečasovaná bisimulační ekvivalence.Konstrukce regionů (regions) u časovaných automatů.HM-logika s časem.Softwarový nástroj UPPAAL (založený na časovaných automatech).Modelování, specifikace, simulace a verifikace v UPPAALu napraktických příkladech.Vyřešení malého projektu: modelování a analýza `drbajících dívek'(gossiping girls) v nástroji UPPAAL.Stručná informace o dalších oblastech verifikace.Shrnutí kursu, podrobné informace o formě a obsahu zkoušky.Cvičení:Procvičení příkladů jednoduchých přechodových systémůa zápisů v CCS.Příklady malých systémů popsaných v CCS. Neformální diskuse(ne)ekvivalence jejich chování.Procvičení pojmu bisimulační ekvivalence formou bisimulačních her na malých přechodových systémech.Důkazy ekvivalentního chování vzhledem k slabé bisimulačníekvivalenci - pro malé systémy s tužkou a papírem.Vyjadřování jednoduchých vlastností v HM-logice.Praktické uvedení softwarového nástroje CWB.Procvičení významu (sémantiky) rekurzivních programů pomocívýpočtu pevného bodu.Příklady HML-formulí s rekurzí. Příprava na první malý projekt (protokol s alternujícím bitem).Dokončení projektu modelování a verifikace protokolu s alternujícím bitem(v nástroji CWB).Příklady modelů malých systémů s časem, popsaných v časovaném CCS a pomocí časovaných automatů.Příklady ekvivalentních systémů z hlediska časované bisimulačníekvivalence. Výpočet regionů (regions) u časovaných automatů.Praktické uvedení softwarového nástroje UPPAAL.Příprava na druhý malý projekt (problém `drbajících dívek').Dokončení projektu modelování a verifikace problému `drbajících dívek'(v nástroji UPPAAL).Shrnutí vyřešených příkladů a miniprojektů a diskuseklíč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í.

Literatura

Luca Aceto, Anna Ingólfsdóttir, Kim G. Larsen and Jiří Srba: Reactive Systems: Modelling, Specification and Verification.Cambridge University Press, August 2007.Gerd Behrmann, Alexandre David, Kim G. Larsen: A Tutorial on Uppaal 4.0. Dostupné online na http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf[12.9.2014]

Požadavky

Žádné

Garant

Ing. Martin Kot, Ph.D.

Vyučující

Ing. Martin Kot, Ph.D.