Formální verifikace a simulace pro tvorbu bezpečných systémů
Skupina se zaměřuje na výzkum metod modelem řízeného návrhu a automatizované verifikace umožňujících zvýšení spolehlivosti a bezpečnosti počítačových systémů. Zkoumané metody modelem řízeného návrhu staví na vysokoúrovňových návrhových jazycích s grafickou reprezentací modelů a rigorózními formálními základy, jako jsou různé typy
Petriho sítí nebo
DEVS. Zvláštní aplikační doménou je zde přitom zejména oblast návrhu inteligentních systémů, systémů bez jasné specifikace, a/nebo systémů s agenty. Výzkum metod verifikace systémů zahrnuje jak přístupy založené na simulaci a testování (resp. dynamické analýze), tak přístupy
formální verifikace založené na statické analýze či model checkingu konečně i nekonečně stavových systémů. V posledním jmenovaném případě jsou intenzivně využívány (a dále rozvíjeny) poznatky z oblasti formálních jazyků, automatů a logik. Mimo metod automatické verifikace, resp. vyhledávání chyb v systémech, se skupina zabývá též zkoumáním metod
automatického opravování chyb nalezených v systémech.
