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í
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 14+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:

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

Prezenční forma (platnost od: 2020/2021 zimní semestr)
Název úlohyTyp úlohyMax. počet bodů
(akt. za podúlohy)		Min. počet bodůMax. počet pokusů
Zápočet a zkouška Zápočet a zkouška 100 (100) 51
        Zápočet Zápočet 30 (30) 10
                1. praktická úloha (práce s nástrojem CAAL) Jiný typ úlohy 15  10
                2. praktická úloha (práce s nástrojem UPPAAL) Jiný typ úlohy 15  10
        Zkouška Zkouška 70  25 3
Rozsah povinné účasti: Účast na cvičeních je povinná a je kontrolována. S rozsahem povinné účastí seznámí studenty garant předmětu na začátku semestru.

Zobrazit historii

Podmínky absolvování předmětu a účast na cvičeních v rámci ISP: Splnění všech povinných úkolů v individuálně dohodnutých termínech. Rozsah účasti na cvičeních si student na začátku semestru dohodne s garantem předmětu.

Zobrazit historii
Kombinovaná forma (platnost od: 2020/2021 zimní semestr)
Název úlohyTyp úlohyMax. počet bodů
(akt. za podúlohy)		Min. počet bodůMax. počet pokusů
Zápočet a zkouška Zápočet a zkouška 100 (100) 51
        Zápočet Zápočet 30 (30) 10
                1. praktická úloha (práce s nástrojem CAAL) Jiný typ úlohy 15  10
                2. praktická úloha (práce s nástrojem UPPAAL) Jiný typ úlohy 15  10
        Zkouška Zkouška 70  25 3
Rozsah povinné účasti: Účast na tutoriálech je povinná a je kontrolována. S rozsahem povinné účastí seznámí studenty garant předmětu na začátku semestru.

Zobrazit historii

Podmínky absolvování předmětu a účast na cvičeních v rámci ISP: Splnění všech povinných úkolů v individuálně dohodnutých termínech.

Zobrazit historii

Výskyt ve studijních plánech

Akademický rokProgramObor/spec.Spec.ZaměřeníFormaJazyk výuky Konz. stř.RočníkZLTyp povinnosti
2025/2026 (N0613A140034) Informatika TI P čeština Ostrava 1 povinně volitelný typu B stu. plán
2025/2026 (N0613A140034) Informatika TI K čeština Ostrava 1 povinně volitelný typu B stu. plán
2024/2025 (N0613A140034) Informatika TI P čeština Ostrava 1 povinně volitelný typu B stu. plán
2024/2025 (N0613A140034) Informatika TI K čeština Ostrava 1 povinně volitelný typu B stu. plán
2023/2024 (N0613A140034) Informatika TI K čeština Ostrava 1 povinně volitelný typu B stu. plán
2023/2024 (N0613A140034) Informatika TI P čeština Ostrava 1 povinně volitelný typu B stu. plán
2023/2024 (N2647) Informační a komunikační technologie (2612T025) Informatika a výpočetní technika P čeština Ostrava 1 povinně volitelný stu. plán
2023/2024 (N2647) Informační a komunikační technologie (2612T025) Informatika a výpočetní technika K čeština Ostrava 1 povinně volitelný stu. plán
2022/2023 (N0613A140034) Informatika TI K čeština Ostrava 1 povinně volitelný typu B stu. plán
2022/2023 (N0613A140034) Informatika TI P čeština Ostrava 1 povinně volitelný typu B stu. plán
2022/2023 (N2647) Informační a komunikační technologie (2612T025) Informatika a výpočetní technika P čeština Ostrava 1 povinně volitelný stu. plán
2022/2023 (N2647) Informační a komunikační technologie (2612T025) Informatika a výpočetní technika K čeština Ostrava 1 povinně volitelný stu. plán
2021/2022 (N2647) Informační a komunikační technologie (2612T025) Informatika a výpočetní technika P čeština Ostrava 1 povinně volitelný stu. plán
2021/2022 (N2647) Informační a komunikační technologie (2612T025) Informatika a výpočetní technika K čeština Ostrava 1 povinně volitelný stu. plán
2020/2021 (N2647) Informační a komunikační technologie (2612T025) Informatika a výpočetní technika P čeština Ostrava 1 povinně volitelný stu. plán
2020/2021 (N2647) Informační a komunikační technologie (2612T025) Informatika a výpočetní technika K č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 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

Hodnocení Výuky



2020/2021 letní
2014/2015 zimní
2011/2012 zimní