456-0358/01 – Modelování a verifikace (MaV)

Garantující katedraKatedra informatikyKredity4
Garant předmětuprof. RNDr. Petr Jančar, CSc.Garant verze předmětuprof. RNDr. Petr Jančar, CSc.
Úroveň studiapregraduální nebo graduálníPovinnostvolitelný odborný
Ročník1Semestrzimní
Jazyk výukyčeština
Rok zavedení2007/2008Rok zrušení2009/2010
Určeno pro fakultyFEIUrčeno pro typy studianavazující magisterské
Výuku zajišťuje
Os. čís.JménoCvičícíPřednášející
JAN59 prof. RNDr. Petr Jančar, CSc.
KOT06 Ing. Martin Kot, Ph.D.
Rozsah výuky pro formy studia
Forma studiaZp.zak.Rozsah
prezenční Zápočet a zkouška 2+2
kombinovaná Zápočet a zkouška 10+4

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

Prezenční forma (platnost od: 2007/2008 zimní semestr)
Název úlohyTyp úlohyMax. počet bodů
(akt. za podúlohy)
Min. počet bodů
Zápočet a zkouška Zápočet a zkouška 100 (100) 51
        Zápočet Zápočet 30 (30) 10
                První projekt (CWB) Projekt 15  10
                Druhý projekt (UPPAAL) Projekt 15  10
        Zkouška Zkouška 70  25
Rozsah povinné účasti:

Zobrazit historii

Výskyt ve studijních plánech

Akademický rokProgramObor/spec.Spec.FormaJazyk výuky Konz. stř.RočníkZLTyp povinnosti
2009/2010 (N2647) Informační a komunikační technologie (2612T025) Informatika a výpočetní technika P čeština Ostrava 1 volitelný odborný stu. plán
2009/2010 (N2647) Informační a komunikační technologie (2612T025) Informatika a výpočetní technika K čeština Ostrava 1 volitelný odborný stu. plán
2008/2009 (N2647) Informační a komunikační technologie (2612T025) Informatika a výpočetní technika P čeština Ostrava 1 volitelný odborný stu. plán
2008/2009 (N2647) Informační a komunikační technologie (2612T025) Informatika a výpočetní technika K čeština Ostrava 1 volitelný odborný stu. plán
2007/2008 (N2647) Informační a komunikační technologie (2612T025) Informatika a výpočetní technika P čeština Ostrava 1 volitelný odborný stu. plán
2007/2008 (N2647) Informační a komunikační technologie (2612T025) Informatika a výpočetní technika K čeština Ostrava 1 volitelný odborný stu. plán

Výskyt ve speciálních blocích

Název blokuAkademický rokForma studiaJazyk výuky RočníkZLTyp blokuVlastník bloku