Detail předmětu

Formální analýza a verifikace

FIT-FAVAk. rok: 2009/2010

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.).

Jazyk výuky

čeština

Počet kreditů

5

Garant předmětu

prof. Ing. Tomáš Vojnar, Ph.D.

Zajišťuje ústav

Ústav inteligentních systémů (UITS)

Výsledky učení 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í.

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.

Prerekvizity

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

Způsob a kritéria hodnocení

Hodnocení studia je založeno na bodovacím systému. Pro úspěšné absolvování předmětu je nutno dosáhnout 50 bodů.

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

Osnovy výuky

  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.

Učební cíle

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, ...).

Vymezení kontrolované výuky a způsob jejího provádění a formy nahrazování zameškané výuky

  • 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ů.

Základní literatura

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. Khedker, U., Sanyal, A., Sathe, B.: Data Flow Analysis: Theory and Practice, CRC Press, 2009.

Doporučená literatura

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. Khedker, U., Sanyal, A., Sathe, B.: Data Flow Analysis: Theory and Practice, CRC Press, 2009. Kroening, D., Strichman, O.: Decision Procedures: An Algorithmic Point of View, Springer, 2008. Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual, Addison-Wesley Professional, 2003. Ben-Ari, M.: Principles of the Spin Model Checker, Springer, 2008. Bertot Y., Castéran, P.: Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions, Springer, 2010. 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.

Zařazení předmětu ve studijních plánech

  • Program IT-MGR-2 magisterský navazující

    obor MBI , 0 ročník, zimní semestr, volitelný
    obor MBS , 0 ročník, zimní semestr, povinně volitelný
    obor MGM , 0 ročník, zimní semestr, volitelný
    obor MGM , 0 ročník, zimní semestr, volitelný
    obor MIN , 0 ročník, zimní semestr, povinně volitelný
    obor MIN , 2 ročník, zimní semestr, volitelný
    obor MIS , 0 ročník, zimní semestr, povinně volitelný
    obor MIS , 0 ročník, zimní semestr, volitelný
    obor MMI , 0 ročník, zimní semestr, volitelný
    obor MMM , 1 ročník, zimní semestr, povinný
    obor MPS , 2 ročník, zimní semestr, volitelný
    obor MPV , 0 ročník, zimní semestr, volitelný
    obor MSK , 2 ročník, zimní semestr, povinně volitelný

Typ (způsob) výuky

 

Přednáška

26 hod., nepovinná

Vyučující / Lektor

prof. Ing. Tomáš Vojnar, Ph.D.

Osnova

  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.

Projekt

26 hod., nepovinná

Vyučující / Lektor

prof. Ing. Tomáš Vojnar, Ph.D.