Název:

Formální analýza a verifikace

Zkratka:FAV
Ak.rok:2007/2008
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í:zkouška (ústní)
Výuka:
hod./sempřednáškasem./cvič.lab. cvič.poč. cvič.jiná
Rozsah:2600026
 zkouškatestycvičenílaboratořeostatní
Body:6000040
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 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 (Intel, Nasa, Microsoft, Ericsson, Nokia, ...).
Anotace:
  Formální analýza a verifikace systémů jako možná alternativa a/nebo doplněk k simulaci systémů. Základní seznámení s prostředky, metodami a možnostmi formální analýzy a verifikace. Vybrané modelovací, dotazovací a specifikační jazyky. Stavové prostory a jejich využití pro formální analýzu a verifikaci. Vybrané metody redukce stavových prostorů. Přehled oblastí, ve kterých byly v praxi úspěšně aplikovány metody formální analýzy a verifikace. Stručný popis několika vyspělých nástrojů pro formální analýzu a verifikaci: Spin, Slam, Java PathFinder, Blast, SMV 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.). Automatizované dokazování teorémů.
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ů, jenž 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í pojmu "formální analýza a verifikace". Možnosti a přínos formální analýzy a verifikace. Struktura (automatizovaného) procesu formální analýzy a verifikace. Dokazování teorémů, použití stavových prostorů, stavová exploze.
  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ů (sítě konečných automatů, Petriho sítě, specialiazované paralelní jazyky, aj.). Specifikační a dotazovací jazyky. Statistiky na úrovni stavových prostorů a modelovacích jazyků. Instrumentace modelů, Büchiho automaty, testery.
  4. Temporální logiky. LTL, CTL, CTL*, mí-kalkul. Vztah temporálních logik a automatů. Indexované temporální logiky.
  5. Procesní algebry. Zobecněný pohled na procesní algebry, jejich vztah ke stavovým prostorům, operátory paralelní kompozice a ukrývání. Různé typy ekvivalencí a uspořádání procesů, možnosti jejich ověřování.
  6. Výpočetní složitost analýzy a verifikace. Složitost ve vztahu k velikosti stavových prostorů a ve vztahu k velikosti modelů. Souvislost paměťových a časových nároků metod formální analýzy a verifikace.
  7. Redukce stavových prostorů. 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 modelů, úpravy modelů. Kompozicionalita.
  8. Redukce stavových prostorů. Binární rozhodovací diagramy a symbolické metody. Hashování stavů na jeden bit. Redukce stavových prostorů na základě symetrií v chování modelovaných systémů 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, Java PathFinder, Zing, SMV aj. (dle aktuální situace v oboru).
  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. Bezpečnost, živost a realizovatelnost v reálném čase. Modelovací a specifikační jazyky v oblasti reálného času, časované automaty, temporální logiky s reálným časem.
  12. Práce se stavovými prostory systémů pracujících v reálném čase, regiony, zóny. Automatizované nástroje pro formální analýzu a verifikaci systémů s reálným časem (Uppaal, Kronos, TReX, ...) a jejich aplikace. 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, SMV, JPF, INA, Uppaal, TReX, PVS aj.).
Literatura referenční:
 
  • Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, 2008.
  • Edmund, M.C., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, 2000.
  • 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.
Literatura studijní:
 
  • Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, 2008.
  • Edmund, M.C., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, 2000.
  • 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.
  • Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice Hall, 1991. (Publikace volně dostupná na Internetu.)
  • 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:
  
  • Dva opravované domácí úlohy - každý za 15 bodů.
  • Závěrečná písemná zkouška - 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 domácích úkolů.
 

Vaše IPv4 adresa: 54.152.38.154