Název:

Formální analýza a verifikace

Zkratka:FAV
Ak.rok:2006/2007 (není otevřen)
Semestr:zimní
Studijní plán:
ProgramObor/
specializace
RočníkPovinnost
IT-MGR-2MGM.-volitelný
IT-MGR-2MIN.2.volitelný
IT-MGR-2MIS.-volitelný
IT-MGR-2MPS2.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 (písemná)
Výuka:
hod./sempřednáškasem./cvič.lab. cvič.poč. cvič.jiná
Rozsah:3900013
 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ě
 
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.).
Anotace:
  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ů.
Získané dovednosti, znalosti a kompetence:
  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í.
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.).
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
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
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ů.
 

Vaše IPv4 adresa: 3.90.45.27