460-4016/01 – Modelování a verifikace (MaV)

Garantující katedraKatedra informatikyKredity4
Garant předmětuIng. Martin Kot, Ph.D.Garant verze předmětuIng. Martin Kot, Ph.D.
Úroveň studiapregraduální nebo graduálníPovinnostvolitelný odborný
RočníkSemestrzimní
Jazyk výukyčeština
Rok zavedení2010/2011Rok zrušení
Určeno pro fakultyFEIUrčeno pro typy studianavazující magisterské
Výuku zajišťuje
Os. čís.JménoCvičícíPřednášející
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ě)

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

Doporučená literatura:

Gerard J. Holzmann: The SPIN MODEL CHECKER: Primer and Reference Manual. Addison-Wesley, 2003 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 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

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: Ú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: 2010/2011 zimní semestr, platnost do: 2015/2016 letní 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
2019/2020 (N2647) Informační a komunikační technologie (2612T025) Informatika a výpočetní technika P čeština Ostrava 1 povinně volitelný stu. plán
2019/2020 (N2647) Informační a komunikační technologie (2612T025) Informatika a výpočetní technika K čeština Ostrava 1 povinně volitelný stu. plán
2018/2019 (N2647) Informační a komunikační technologie (2612T025) Informatika a výpočetní technika P čeština Ostrava 1 povinně volitelný stu. plán
2018/2019 (N2647) Informační a komunikační technologie (2612T025) Informatika a výpočetní technika K čeština Ostrava 1 povinně volitelný stu. plán
2017/2018 (N2647) Informační a komunikační technologie (2612T025) Informatika a výpočetní technika P čeština Ostrava 1 povinně volitelný stu. plán
2017/2018 (N2647) Informační a komunikační technologie (2612T025) Informatika a výpočetní technika K čeština Ostrava 1 povinně volitelný stu. plán
2016/2017 (N2647) Informační a komunikační technologie (2612T025) Informatika a výpočetní technika P čeština Ostrava 1 povinně volitelný stu. plán
2016/2017 (N2647) Informační a komunikační technologie (2612T025) Informatika a výpočetní technika K čeština Ostrava 1 povinně volitelný stu. plán
2015/2016 (N2647) Informační a komunikační technologie (2612T025) Informatika a výpočetní technika P čeština Ostrava 1 povinně volitelný stu. plán
2015/2016 (N2647) Informační a komunikační technologie (2612T025) Informatika a výpočetní technika K čeština Ostrava 1 povinně volitelný stu. plán
2014/2015 (N2647) Informační a komunikační technologie (2612T025) Informatika a výpočetní technika P čeština Ostrava 2 volitelný odborný stu. plán
2014/2015 (N2647) Informační a komunikační technologie (2612T025) Informatika a výpočetní technika K čeština Ostrava 1 volitelný odborný stu. plán
2013/2014 (N2647) Informační a komunikační technologie (2612T025) Informatika a výpočetní technika P čeština Ostrava 2 volitelný odborný stu. plán
2013/2014 (N2647) Informační a komunikační technologie (2612T025) Informatika a výpočetní technika K čeština Ostrava 1 volitelný odborný stu. plán
2012/2013 (N2647) Informační a komunikační technologie (2612T025) Informatika a výpočetní technika P čeština Ostrava 2 volitelný odborný stu. plán
2012/2013 (N2647) Informační a komunikační technologie (2612T025) Informatika a výpočetní technika K čeština Ostrava 1 volitelný odborný stu. plán
2011/2012 (N2647) Informační a komunikační technologie (2612T025) Informatika a výpočetní technika P čeština Ostrava 1 volitelný odborný stu. plán
2011/2012 (N2647) Informační a komunikační technologie (2612T025) Informatika a výpočetní technika K čeština Ostrava 1 volitelný odborný stu. plán
2010/2011 (N2647) Informační a komunikační technologie (2612T025) Informatika a výpočetní technika P čeština Ostrava 1 volitelný odborný stu. plán
2010/2011 (N2647) Informační a komunikační technologie (2612T025) Informatika a výpočetní technika K čeština Ostrava 1 volitelný odborný stu. plán
2010/2011 (N2647) Informační a komunikační technologie (2612T025) Informatika a výpočetní technika (01) Exchange Students P čeština Ostrava volitelný odborný stu. plán
2010/2011 (B2649) Elektrotechnika (2601R004) Měřicí a řídicí technika (01) Exchange Students P čeština Ostrava volitelný odborný stu. plán
2010/2011 (B2649) Elektrotechnika (2602R014) Aplikovaná a komerční elektronika (01) Exchange Students P čeština Ostrava volitelný odborný stu. plán
2010/2011 (B2649) Elektrotechnika (3901R039) Biomedicínský technik (01) Exchange Students P čeština Ostrava volitelný odborný stu. plán
2010/2011 (B2649) Elektrotechnika (3907R001) Elektroenergetika (01) Exchange Students P čeština Ostrava volitelný odborný stu. plán
2010/2011 (B2647) Informační a komunikační technologie (1103R031) Výpočetní matematika (01) Exchange Students P čeština Ostrava volitelný odborný stu. plán
2010/2011 (B2647) Informační a komunikační technologie (2601R013) Telekomunikační technika (01) Exchange Students P čeština Ostrava volitelný odborný stu. plán
2010/2011 (B2647) Informační a komunikační technologie (2612R025) Informatika a výpočetní technika (01) Exchange Students P čeština Ostrava volitelný odborný stu. plán
2010/2011 (B2647) Informační a komunikační technologie (2612R059) Mobilní technologie (01) Exchange Students P čeština Ostrava volitelný odborný stu. plán
2010/2011 (N2647) Informační a komunikační technologie (1103T031) Výpočetní matematika (01) Exchange Students P čeština Ostrava volitelný odborný stu. plán
2010/2011 (N2647) Informační a komunikační technologie (2601T013) Telekomunikační technika (01) Exchange Students P čeština Ostrava volitelný odborný stu. plán
2010/2011 (N2647) Informační a komunikační technologie (2612T059) Mobilní technologie (01) Exchange Students P čeština Ostrava volitelný odborný stu. plán
2010/2011 (N2649) Elektrotechnika (2601T004) Měřicí a řídicí technika (01) Exchange Students P čeština Ostrava volitelný odborný stu. plán
2010/2011 (N2649) Elektrotechnika (2612T015) Elektronika (01) Exchange Students P čeština Ostrava volitelný odborný stu. plán
2010/2011 (N2649) Elektrotechnika (3901T009) Biomedicínské inženýrství (01) Exchange Students P čeština Ostrava volitelný odborný stu. plán
2010/2011 (N2649) Elektrotechnika (3907T001) Elektroenergetika (01) Exchange Students P čeština Ostrava 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