Název:

Formální analýza a verifikace

Zkratka:FAV
Ak.rok:2009/2010
Semestr:zimní
Studijní plán:
ProgramOborRočníkPovinnost
IT-MGR-2MBI-volitelný
IT-MGR-2MBS-povinně volitelný - skupina B
IT-MGR-2MGM-volitelný
IT-MGR-2MGM.-volitelný
IT-MGR-2MIN-povinně volitelný - skupina B
IT-MGR-2MIN.2.volitelný
IT-MGR-2MIS-povinně volitelný - skupina F
IT-MGR-2MIS.-volitelný
IT-MGR-2MMI-volitelný
IT-MGR-2MMM1.povinný
IT-MGR-2MPS2.volitelný
IT-MGR-2MPV-volitelný
IT-MGR-2MSK2.povinně volitelný - skupina M
IT-MGR-2EITE2.volitelný
Vyučovací jazyk:čeština, angličtina
Informace veřejné:http://www.fit.vutbr.cz/study/courses/FAV/public/
Kredity:5 kreditů
Ukončení:zápočet+zkouška (kombinovaná)
Výuka:
hod./sempřednáškasem./cvičenílab. cvičenípoč. cvičeníjiná
Rozsah:2600026
 zkouškatestycvičenílaboratořeostatní
Body:7000030
Garant:Vojnar Tomáš, prof. Ing., Ph.D., UITS
Přednášející:Vojnar Tomáš, prof. Ing., Ph.D., UITS
Fakulta:Fakulta informačních technologií VUT v Brně
Pracoviště:Ústav inteligentních systémů FIT VUT v Brně
Prerekvizity: 
Algoritmy (IAL), UIFS
Formální jazyky a překladače (IFJ), UIFS
 
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, ...).
Anotace:
  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). Formální analýza a verifikace systémů pracujících v reálném čase (systémy Uppaal, Kronos, HyTech, TReX apod.).
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.
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.
Osnova přednášek:
 
  1. Vymezení pojmů formální analýza 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*.
  4. Model checking systémů s vlastnostmi specifikovanými v CTL* s využitím explicitně reprezentovaných stavových prostorů.
  5. Binární rozhodovací diagramy pro úspornou symbolickou reprezentaci stavových prostorů a jejich implementace.
  6. Svazy, pevné body, Knaster-Tarského věta jako teoretický základ pro symbolický model checking.
  7. Symbolický model checking pro CTL a CTL*.
  8. 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ů.
  9. 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 vyrovnávání se se stavovou explozí.
  10. 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.
  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.  Stručná zmínka o abstraktní interpretaci a jejím využití pro definici statických analýz.
  12. Statická analýza založená na vyhledávání chybových vzorů.
  13. 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).
Osnova ostatní - projekty, práce:
 
  • 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).
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.
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.
Průběžná kontrola studia:
  
  • 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.
  • 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 projektu.