Detail předmětu

Formální analýza a verifikace

FIT-FAVAk. rok: 2018/2019

Formální analýza a verifikace systémů jako moderní alternativa a/nebo doplněk k simulaci a testování systémů. Vybrané formalismy pro specifikaci ověřovaných vlastností. Model checking: formální verifikace založená na systematickém zkoumání stavových prostorů ověřovaných systémů. Různé přístupy k redukci stavových prostorů, zejména pak redukce založená na částečném uspořádaní akcí. Metody automatické abstrakce zkoumaných systémů, zejména pak predikátová abstrakce. 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).

Jazyk výuky

čeština

Počet kreditů

5

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í

Jeden opravovaný projekt za 30 bodů. Závěrečná zkouška za 70 bodů. Podmínka zápočtu: min. 15 bodů získaných v průběhu semestru.
Podmínky zápočtu:
Získání alespoň 50% možného bodového zisku z projektu.

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

Doporučená literatura

Aho, A.V., Lam, S., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools. Addison Wesley, 2nd ed., 2006. The part devoted to static analysis.
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.
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.
Materials presented within the lectures and made accessible via the Internet.
Materials freely accessible on the Internet, especially papers and documentation related to the various computer-aided tools for formal analysis and verification.
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.

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

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

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

Typ (způsob) výuky

 

Přednáška

39 hod., nepovinná

Vyučující / Lektor

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.
  6. Symbolický model checking pro CTL a CTL*.
  7. 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ů.
  8. Redukce stavových prostorů na základě částečného uspořádaní akcí prováděných systémem. Přehled dalších přístupů k redukci stavových prostorů (symetrie, kompozitní verifikace apod.).
  9. 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.
  10. 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).
  11. 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.
  12. Abstraktní interpretace a její využití pro definici statických analýz.
  13. Statická analýza založená na vyhledávání chybových vzorů, zmínka o metodách dynamické analýzy (zejména pro potřeby detekce chyb v paralelismech).

Projekt

13 hod., povinná

Vyučující / Lektor

Osnova

  • Projekt zahrnující nainstalování zvoleného nástroje pro automatickou verifikaci na formálním základě (Spin, Blast, ARMC, SMV, JPF, FindBugs, Invader, Uppaal aj.), experimenty s tímto nástrojem a sepsání eseje krátce popisující princip činnosti zvoleného nástroje (10b.) a provedené experimenty (10b. za experimenty na stávajících případových studiích, 10b. za nové případové studie). Po domluvě je možno se zaměřit i na nástroj založený na principech, které nejsou součástí přednášek (dokazování teorémů, systémy pracující v reálném časy apod.).