Přístupnostní navigace
E-přihláška
Vyhledávání Vyhledat Zavřít
Detail předmětu
FIT-FAVAk. rok: 2010/2011
Formální analýza a verifikace systémů jako moderní alternativa a/nebo doplněk k simulaci a testování systémů. Model checking: formální verifikace založená na systematickém zkoumání stavových prostorů ověřovaných systémů. Vybrané modelovací, dotazovací a specifikační jazyky. Různé přístupy k redukci stavových prostorů. Metody automatické abstrakce zkoumaných systémů, zejména pak predikátová abstrakce. Automatizované dokazování teorémů, rozhodovací procedury, 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.).
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
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 , 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 MGM , libovolný ročník, zimní semestr, volitelnýobor MPV , libovolný ročník, zimní semestr, volitelnýobor MMM , 1. ročník, zimní semestr, povinnýobor MSK , 2. ročník, zimní semestr, povinně volitelnýobor MPS , 2. ročník, zimní semestr, volitelný
Přednáška
Vyučující / Lektor
Osnova
Projekt