Fakulta informačních technologií VUT v Brně

Detail předmětu

Formální analýza a verifikace

FAV Ak. rok 2007/2008 zimní semestr 5 kreditů

Formální analýza a verifikace systémů jako možná alternativa a/nebo doplněk k simulaci systémů. Základní seznámení s prostředky, metodami a možnostmi formální analýzy a verifikace. Vybrané modelovací, dotazovací a specifikační jazyky. Stavové prostory a jejich využití pro formální analýzu a verifikaci. Vybrané metody redukce stavových prostorů. Přehled oblastí, ve kterých byly v praxi úspěšně aplikovány metody formální analýzy a verifikace. Stručný popis několika vyspělých nástrojů pro formální analýzu a verifikaci: Spin, Slam, Java PathFinder, Blast, SMV apod. (dle aktuální situace v oboru). Formální analýza a verifikace systémů pracujících v reálném čase (systémy Uppaal, Kronos, HyTech, TReX apod.). Automatizované dokazování teorémů.

Garant předmětu

Jazyk výuky

česky, anglicky

Zakončení

zkouška (ústní)

Rozsah

26 hod. přednášky, 26 hod. projekty

Bodové hodnocení

60 zkouška, 40 projekty

Zajišťuje ústav

Přednášející

Získané dovednosti, znalosti a kompetence z předmětu

Studenti jsou obeznámení s principy a metodami formální analýzy a verifikace a s jejím využitím při návrhu systémů, u nichž je kladen důraz na jejich korektní funkčnost. Studenti znají možnosti a základní způsoby použití počítačových nástrojů, jenž formální analýzu a verifikaci podporují.

Dovednosti, znalosti a kompetence obecné

Získané povědomí o významu a možnostech uplatnění formálních metod při vývoji různých typů systémů a o jejich rostoucím nasazení v praxi.

Cíle předmětu

Cílem předmětu je představit studentům formální analýzu a verifikaci jako moderní a perspektivní metodu automatizovaného ověřování vlastností různých typů systémů, u nichž je kladen důraz na bezchybnou funkci (např. ovladačů a jiných částí operačních systémů, řídících programů, workflow, komunikačních protokolů, částí hardware apod.). Předmět seznamuje studenty jak s teoretickými základy dané oblasti, s počítačovými nástroji na nich založenými, tak i s úspěšnými aplikacemi formální analýzy a verifikace v praxi (Intel, Nasa, Microsoft, Ericsson, Nokia, ...).

Literatura studijní

  • Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, 2008.
  • Edmund, M.C., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, 2000.
  • Valmari, A.: The State Explosion Problem. In Reisig, W., Rozenberg, G.: Lectures on Petri Nets I: Basic Models, volume 1491 of Lecture Notes in Computer Science, pages 429--528. Springer-Verlag, 1998.
  • Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice Hall, 1991. (Publikace volně dostupná na Internetu.)
  • Soubor materiálů prezentovaných na přednáškách a zveřejněných přes WWW.
  • Materiály aktuálně volně dostupné na Internetu, a to zejména články a dokumentace týkající se počítačových nástrojů pro formální analýzu a verifikaci.

Literatura referenční

  • Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, 2008.
  • Edmund, M.C., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, 2000.
  • Valmari, A.: The State Explosion Problem. In Reisig, W., Rozenberg, G.: Lectures on Petri Nets I: Basic Models, volume 1491 of Lecture Notes in Computer Science, pages 429--528. Springer-Verlag, 1998.

Osnova přednášek

  1. Vymezení pojmu "formální analýza a verifikace". Možnosti a přínos formální analýzy a verifikace. Struktura (automatizovaného) procesu formální analýzy a verifikace. Dokazování teorémů, použití stavových prostorů, stavová exploze.
  2. Stavový prostor, cesty stavovým prostorem, abstrakce stavů a přechodů. Prokládání a paralelismus. Lineární a větvící se logický čas. Bezpečnost, živost a spravedlivost.
  3. Stručný přehled běžně používaných modelovacích jazyků (sítě konečných automatů, Petriho sítě, specialiazované paralelní jazyky, aj.). Specifikační a dotazovací jazyky. Statistiky na úrovni stavových prostorů a modelovacích jazyků. Instrumentace modelů, Büchiho automaty, testery.
  4. Temporální logiky. LTL, CTL, CTL*, mí-kalkul. Vztah temporálních logik a automatů. Indexované temporální logiky.
  5. Procesní algebry. Zobecněný pohled na procesní algebry, jejich vztah ke stavovým prostorům, operátory paralelní kompozice a ukrývání. Různé typy ekvivalencí a uspořádání procesů, možnosti jejich ověřování.
  6. Výpočetní složitost analýzy a verifikace. Složitost ve vztahu k velikosti stavových prostorů a ve vztahu k velikosti modelů. Souvislost paměťových a časových nároků metod formální analýzy a verifikace.
  7. Redukce stavových prostorů. Přehled různých přístupů k redukci stavových prostorů, propojení algoritmů redukce a algoritmů generování a využití stavových prostorů. Abstrakce modelů, úpravy modelů. Kompozicionalita.
  8. Redukce stavových prostorů. Binární rozhodovací diagramy a symbolické metody. Hashování stavů na jeden bit. Redukce stavových prostorů na základě symetrií v chování modelovaných systémů a na základě částečného uspořádání akcí.
  9. Počítačové nástroje podporující formální analýzu a verifikaci založenou na využití stavových prostorů. Spin, Slam, Java PathFinder, Zing, SMV aj. (dle aktuální situace v oboru).
  10. Přehled úspěšných aplikací formální analýzy a verifikace v oblasti vestavěných systémů, protokolového inženýrství, řídicích systémů, workflow systémů, apod.
  11. Systémy pracující v reálném čase. Logický a fyzický čas. Bezpečnost, živost a realizovatelnost v reálném čase. Modelovací a specifikační jazyky v oblasti reálného času, časované automaty, temporální logiky s reálným časem.
  12. Práce se stavovými prostory systémů pracujících v reálném čase, regiony, zóny. Automatizované nástroje pro formální analýzu a verifikaci systémů s reálným časem (Uppaal, Kronos, TReX, ...) a jejich aplikace. Hybridní systémy (HyTech).
  13. Dokazování teorémů. Principy, automatizovaná podpora (PVS, aj.), aplikace. Kombinace dokazování teorémů a metod založených na stavových prostorech.

Osnova ostatní - projekty, práce

  • Dvě domácí úlohy zaměřené na vytvoření modelu jednoduchého systému a ověření jeho chování ve dvou zvolených nástrojích pro formální analýzu a verifikaci (Spin, Zing, SMV, JPF, INA, Uppaal, TReX, PVS aj.).

Průběžná kontrola studia

  • Dva opravované domácí úlohy - každý za 15 bodů.
  • Závěrečná písemná zkouška - 70 bodů.
  • Podmínka zápočtu: min. 15 bodů získaných v průběhu semestru.
  • Hranice pro úspěšnou zkoušku podle pravidel ECTS - 50 bodů.

Podmínky zápočtu

Získání alespoň 50% možného bodového zisku z domácích úkolů.
Nahoru