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

Detail předmětu

Formální analýza a verifikace

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

Formální analýza a verifikace systémů jako moderní alternativa a/nebo doplněk k simulaci a testování systémů. Model checking: formální verifikace založená na systematickém zkoumání stavových prostorů ověřovaných systémů. Vybrané modelovací, dotazovací a specifikační jazyky. Různé přístupy k redukci stavových prostorů. Metody automatické abstrakce zkoumaných systémů, zejména pak predikátová abstrakce. Automatizované dokazování teorémů, rozhodovací procedury, moderní metody řešení problémů SAT a SMT a jejich aplikace ve formální analýze a verifikaci. Statická analýza založená na vyhledávání chybových vzorů, analýze toku dat a abstraktní interpretaci. Stručný popis několika vyspělých nástrojů pro formální analýzu a verifikaci: SMV, Spin, Slam, Blast, Java PathFinder, ARMC, FindBugs 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.).

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ů, které 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 (Microsoft, Intel, Nasa, Airbus, ...).

Požadované prerekvizitní znalosti a dovednosti

Předpokládají se znalosti diskrétní matematiky, teorie formálních jazyků a algoritmizace na bakalářské úrovni.

Literatura studijní

  • Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, 2008.
  • Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis, Springer-Verlag, 2005.
  • Edmund, M.C., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, 2000.
  • Aho, A.V., Lam, S., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools. Addison Wesley, 2nd ed., 2006. (Část věnovaná statické analýze.)
  • Bradley, A.R., Manna, Z.: The Calculus of Computation: Decision Procedures with Applications to Verification, Springer, 2007.
  • 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.
  • Chess, B., West,J.: Secure Programming with Static Analysis. Addison-Wesley Professional, 2007.
  • 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.
  • Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis, Springer-Verlag, 2005.
  • Edmund, M.C., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, 2000.

Osnova přednášek

  1. Vymezení pojmu "formální analýza a verifikace". Možnosti a přínos formální analýzy a verifikace. Různé přístupy k formální analýze a verifikaci: model checking, statická analýza, dokazování teorémů.
  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. Temporální logiky CTL a CTL*, model checking systémů s vlastnostmi specifikovanými v těchto logikách s využitím explicitně reprezentovaných stavových prostorů.
  4. Binární rozhodovací diagramy pro úspornou symbolickou reprezentaci stavových prostorů a jejich implementace.
  5. Svazy, pevné body, Knaster-Tarského věta jako teoretický základ pro symbolický model checking. Symbolický model checking pro CTL a CTL*.
  6. Temporální logika LTL, korespondence mezi Büchi automaty a formulemi LTL, model checking systémů s vlastnostmi specifikovanými v LTL s využitím Büchiho automatů.
  7. Redukce stavových prostorů na základě částečného uspořádaní akcí prováděných systémem. Redukce stavových prostorů na základě symetrií. Přehled dalších přístupů k redukci stavových prostorů. Kompozitní verifikace.
  8. Metody automatizované abstrakce systémů, predikátová abstrakce, postupné zjemňování abstrakce na základě vylučování chybných protipříkladů, Craigova interpolace.
  9. Rozhodovací procedury a moderní metody řešení problémů SAT a SMT a jejich využití ve formální verifikaci (např. v rámci predikátové abstrakce).
  10. Klasické analýzy toku dat (živé proměnné, dostupné výrazy apod.) i některé vybrané pokročilé analýzy toku dat (např. některé analýzy ukazatelů), jejich popis pomocí tokových rovnic, metody iterativního řešení těchto rovnic.
  11. Zmínka o abstraktní interpretaci a jejím využití pro definici statických analýz. Statická analýza založená na vyhledávání chybových vzorů.
  12. Systémy pracující v reálném čase a jejich formální verifikace, zejména s využitím časovaných automatů a symbolických metod založených na regionech či zónách.
  13. Dokazování teorémů. Principy, automatizovaná podpora. 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 verifikaci jednoduchého systému ve dvou zvolených nástrojích pro formální analýzu a verifikaci (Spin, Blast, ARMC, SMV, JPF, Uppaal, TReX, PVS, FindBugs aj.).

Průběžná kontrola studia

  • Dvě opravované domácí úlohy - každá za 20 bodů.
  • Závěrečná zkouška - 60 bodů.
  • Podmínka zápočtu: min. 20 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