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

Detail předmětu

Formální analýza a verifikace

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

Předmět není v tomto roce otevřen
Zavřít
Formální analýza a verifikace jsou moderními a rychle se rozvíjejícími přístupy k rigoróznímu ověřování korektnosti počítačových systémů. Předmět Formální analýza a verifikace 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. Důraz je kladen na metody založené na práci se stavovými prostory, jež nabízejí v praxi velice vítanou vysokou míru automatizace. Předmět pokrývá různé způsoby efektivního generování, redukce a využití stavových prostorů systémů logického i reálného času. Na závěr je pak jako alternativa k využití stavových prostorů zmíněna metoda dokazování teorémů.

Garant předmětu

Jazyk výuky

česky, anglicky

Zakončení

zápočet+zkouška (písemná)

Rozsah

39 hod. přednášky, 13 hod. projekty

Bodové hodnocení

70 zkouška, 30 projekty

Zajišťuje ústav

Přednášející

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

Znalost principů a metod formální analýzy a verifikace a možností jejich využití při návrhu počítačových systémů. Znalost vybraných počítačových nástrojů, jež formální analýzu a verifikaci podporují.

Cíle předmětu

Cílem předmětu je seznámit studenty s formální analýzou a verifikací jako s moderní a perspektivní metodou 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.).

Literatura studijní

  • Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, 2000. ISBN 0-262-03270-8
  • Berard, B., Bidoit, M., Finkel, A., Laroussinie, F., Petit, A., Petrucci, L., Schnoebelen, P., McKenzie, P.: Systems and Software Verification: Model-Checking Techniques and Tools, Springer-Verlag, 2001. ISBN 3-540-41523-8

Literatura referenční

  • Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking, MIT Press, 2000. ISBN 0-262-03270-8
  • Berard, B., Bidoit, M., Finkel, A., Laroussinie, F., Petit, A., Petrucci, L., Schnoebelen, P., McKenzie, P.: Systems and Software Verification: Model-Checking Techniques and Tools, Springer-Verlag, 2001. ISBN 3-540-41523-8
  • Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual, Addison-Wesley Professional, 2003. ISBN 0-321-22862-6
  • Monin, J.F., Hinchey, M.G.: Understanding Formal Methods, Springer-Verlag, 2003. ISBN 1-852-33247-6
  • Valmari, A.: The State Explosion Problem. In Reisig, W., Rozenberg, G.: Lectures on Petri Nets I: Basic Models, Lecture Notes in Computer Science, č.1491, s. 429-528. Springer-Verlag, 1998. ISBN 3-540-65306-6

Osnova přednášek

  1. Možnosti, přínos a struktura (automatizovaného) procesu formální analýzy a verifikace.
  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ů. Specifikační a dotazovací jazyky. Statistiky nad stavovými prostory, instrumentace modelů, Büchiho automaty, testery.
  4. Temporální logiky. LTL, CTL, CTL*, mí-kalkul. Vztah temporálních logik a automatů.
  5. Procesní algebry. Různé typy relací nad procesy, možnosti jejich ověřování.
  6. Výpočetní složitost problémů formální analýzy a verifikace. 
  7. 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, kompozicionalita.
  8. Binární rozhodovací diagramy a symbolické metody. Hashování stavů na jeden bit. Redukce na základě symetrií 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, Blast, Java PathFinder, Zing, SMV aj.
  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. Modelovací a specifikační jazyky v oblasti reálného času, časované automaty, temporální logiky s reálným časem.
  12. Stavové prostory systémů pracujících v reálném čase, regiony, zóny a automatizované nástroje na nich založené (Uppaal, Kronos, TReX, ...). 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, Blast, SMV, JPF, INA, Uppaal, TReX, PVS aj.).

Průběžná kontrola studia

Dva opravované domácí úlohy.

Podmínky zápočtu

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