456-0358/01 – Modelování a verifikace (MaV)
Garantující katedra | Katedra informatiky | Kredity | 4 |
Garant předmětu | prof. RNDr. Petr Jančar, CSc. | Garant verze předmětu | prof. RNDr. Petr Jančar, CSc. |
Úroveň studia | pregraduální nebo graduální | Povinnost | volitelný odborný |
Ročník | 1 | Semestr | zimní |
| | Jazyk výuky | čeština |
Rok zavedení | 2007/2008 | Rok zrušení | 2009/2010 |
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ě)
Projekt
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:
Luca Aceto, Anna Ingólfsdóttir, Kim G. Larsen and Jiří Srba: Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, August 2007.
Doporučená literatura:
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 individuální písemnou zprávou.
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
Prerekvizity
Předmět nemá žádné prerekvizity.
Korekvizity
Předmět nemá žádné korekvizity.
Osnova předmětu
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ých
vlastností 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 na
praktický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 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