..:: Martin Kot ::..
Modelování a verifikace - šk. rok 2022/23
Obecné Aktuálně Ke stažení
 
Obecné údaje
Garant:  Ing. Martin Kot, Ph.D.
Počet kreditů:  4
Rozsah:  2/2/0/0
Ukončení:  Zkouška
Oficiální stránka:  https://www.cs.vsb.cz/kot/?show=MAV
Přednášející: 
Cvičící: 
 
Rozdělení bodů
Zápočet: 
  • 30b - dva projekty po 15 bodech hodnocených 0 nebo 10-15 bodů
  • Podmínkou na zápočet je získání nenulového počtu bodů z alespoň 1 projektu
Zkouška: 
  • 70b - ústní zkouška
 
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.
 
Rozvrh hodin
7:15
8:00
8:00
8:45
9:00
9:45
9:45
10:30
10:45
11:30
11:30
12:15
12:30
13:15
13:15
14:00
14:15
15:00
15:00
15:45
16:00
16:45
16:45
17:30
17:45
18:30
18:30
19:15
pondělí                            
úterý    
EA408
Kot M.
                   
středa                            
čtvrtek                            
pátek                            
sobota                            
 
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.
 
Studijní literatura
  • Luca Aceto, Anna Ingólfsdóttir, Kim G. Larsen and Jiří Srba: Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, August 2007.
     
    Autoři knihy zřídili webovskou stránku http://rsbook.cs.aau.dk která obsahuje odkazy na další související a užitečné materiály.