Výzkumný záměr

Výzkum informačních technologií z hlediska bezpečnosti 2007 - 2013

Logo FIT VUT

Výzkumný záměr
je řešen na Fakultě
informačních technologií
VUT v Brně

Výzkumná skupina 1Výzkumná skupina 2Výzkumná skupina 3Výzkumná skupina 4Výzkumná skupina 5Výzkumná skupina 6Výzkumná skupina 7

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.