Přístupnostní navigace
E-přihláška
Vyhledávání Vyhledat Zavřít
Detail předmětu
FIT-FAVAk. rok: 2013/2014
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
Počet kreditů
Garant předmětu
Zajišťuje ústav
Výsledky učení předmětu
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
Plánované vzdělávací činnosti a výukové metody
Způsob a kritéria hodnocení
Osnovy výuky
Učební cíle
Vymezení kontrolované výuky a způsob jejího provádění a formy nahrazování zameškané výuky
Základní literatura
Doporučení literatura
Zařazení předmětu ve studijních plánech
obor MBS , 0 ročník, zimní semestr, povinně volitelnýobor MIN , 0 ročník, zimní semestr, povinně volitelnýobor MIS , 0 ročník, zimní semestr, povinně volitelnýobor MMI , 0 ročník, zimní semestr, volitelnýobor MMM , 0 ročník, zimní semestr, povinnýobor MPV , 0 ročník, zimní semestr, volitelnýobor MBI , 0 ročník, zimní semestr, volitelnýobor MGM , 0 ročník, zimní semestr, volitelnýobor MSK , 2 ročník, zimní semestr, povinně volitelný
Přednáška
Vyučující / Lektor
Osnova
Projekt