Požadavky
Tato stránka obsahuje stručný komentář ke zkušebním požadavkům okruhu Modely a verifikace programů.
U jednotlivých požadavků jsou podle potřeby uvedeny heslovité podrobnosti o obsahu a některé základní znalosti, bez kterých zpravidla není možné zkoušku složit.
Je nutné upozornit, že komentář není oficiální, pro potřeby státní zkoušky je závazné pouze oficiální znění zkušebních požadavků a jeho výklad hodnotícími členy zkušební komise !
Matematické struktury pro modelování chování systémů
Přechodové systémy, Kripkeho struktury.
Podrobnosti:
- Vysvětlení konceptů LTS, Kripkeho struktura, abstrakce.
- Porovnávání dvou specifikací různými metodami.
Základy:
- LTS.
- Kripkeho struktura.
- Ekvivalence - simulace, bisimulace, trace evivalence.
Specifikace vlastností systému pomocí temporálních logik
LTL, CTL, CTL*, CTL s fairness constraints.
Podrobnosti:
- Cíl specifikace pomocí temporálních logik.
- Rozdíly mezi jednotlivými logikami, vyjadřovací síla, limity.
- Fairness constraints, jejich využití na praktickém příkladu.
Základy:
- Syntaxe a sémantika LTL, CTL, rozdíly.
Základní verifikační úlohy
Equivalence checking a model checking.
Podrobnosti:
- Definice a vysvětlení základních verifikačních úloh.
- Problémy spojené s praktickou aplikací (abstrakce, state explosion problem, ...).
Základy:
- Equivalence checking, model checking - definice, rozdíly, uplatnění.
Algoritmy pro model checking a různé metody optimalizace
BDD, partial order reduction.
Podrobnosti:
- Ukázat, jak se dají OBDD využít v konkrétní verifikační úloze
- Popis konkrétní partial order reduction (Spin, Java PathFinder, ...).
Základy:
- Princip explicitního a symbolického model checkingu.
- Princip fungování OBDD a partial order reduction.
Paralelní a distribuovaný model checking
Základy:
- Princip, motivace k paralelnímu a distribuovanému model checkingu.
- Problémy spojené s distribucí, nároky, výhody, podmínky fungování.
Specifikace chování real-time systémů, timed automata
Základy:
- Problém specifikace real-time systémů.
- Definice timed automata.
- Verifikační nástroje.
- Aplikace.
Proces-algebry
Podrobnosti:
- Popis sémantiky a vyjadřovací síly vybrané procesní algebry.
- Varianty komunikace procesů.
- Rozdíly mezi CSP a CCS.
Základy:
- Sytax a sémantika CSP, CCS.
- Verifikační úlohy.
- Limity, aplikace.
Behavior protocols
Podrobnosti:
- Popis sémantiky a vyjadřovací síly.
- Odlišnosti od jiných specifikačních formalismů.
Základy:
- Syntaxe, sémantika, operátor consent.
Statická analýza programů
Podrobnosti:
- Rozdíly oproti model checkingu a dokazování vět.
- Základní algoritmus pro analýzu data-flow.
- Reprezentace programu jako graf control-flow.
- Reprezentace informací o programu pomocí svazů a systémů rovnic.
Základy:
- Definice, aplikace v překladačích a verifikaci.
Model checking programů
Podrobnosti:
- Konstrukce stavového protoru ze zdrojového kódu.
- Reprezentace stavu programu v moderních programovacích jazycích.
- Problémy spojené s model checkingem programů a jejich možná řešení.
- Existenční a univerzální abstrakce stavového prostoru, predikátová abstrakce a CEGAR.
Základy:
- Specifika model checkingu programů ve srovnání s obecným model checkingem,přehled.