Techniques avancées pour la vérification de systèmes à nombre d'états infini

Advanced Methods for Automatic Verification of Infinite-state Systems

Pokročilé techniky automatické verifikace nekonečně stavových systémů

grant

formální verifikace, nekonečně stavové systémy, model checking

Efektivita současných technik pro model checking nekonečně stavových systémů je však stále relativně daleko od jejich skutečně praktické aplikovatelnosti a také třídy systémů a jejich ověřovaných vlastností, na které se tyto techniky dají uplatnit, jsou omezené. Cílem tohoto projektu je proto přispět k výzkumu metod model checkingu nekonečně stavových systémů tak, aby byly v co největší míře odstraněny jejich současná omezení jak v oblasti efektivity, tak v oblasti obecnosti. S cílem zvýšit efektivitu současných technik symbolického model checkingu nekonečně stavových systémů budou v projektu konkrétně zkoumány např. techniky symbolického model checkingu založené na nedeterministických konečných automatech, jež by měly umožnit vyhnout se determinizaci, která je jedním z výpočetně nejdražších kroků v rámci současných přístupů. Za tím účelem je zapotřebí vyvinout všechny potřebné operace (jako např. ověřování prázdnosti, inkluze, minimalizace, abstrakce apod.) nad různými používanými typy automatů nad slovy, stromy atd. Pro zvýšení obecnosti současných technik pak projekt zahrne jak výzkum možností verifikace složitějších systémů (např. programů s neomezenými dynamickými datovými strukturami založenými na ukazatelích a současně s neomezenými celočíselnými proměnnými) i výzkum možností ověřování složitějších vlastností než dosud (včetně např. konečnosti výpočtu či vlastností typu živost). Při práci na tomto cíli budou zkoumány různá rozšíření současných automatů a logik (např. kombinace různých tříd automatů a logik popisujících kvalitativní strukturu systému s různými kvantitativními omezeními) a také algoritmy pro práci s takto rozšířenými formalismy, zahrnující např. pokročilé rozhodovací procedury nad logikami, nové metody abstrakce a učení nad automaty apod. Projekt přitom zahrne jak teoretický výzkum nových metod automatické verifikace nekonečně stavových systémů tak také prototypovou implementaci navržených technik tak, aby jejich vlastnosti mohly být ověřeny na vhodných případových studiích systémů s neomezenými a/nebo dynamickými strukturami, případně s parametry.

Vojnar Tomáš, prof. Ing., Ph.D. (UITS) – hlavní řešitel
Bouajjani Ahmed
Češka Milan, prof. RNDr., CSc.
Habermehl Peter
Holík Lukáš, doc. Mgr., Ph.D. (UITS)
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS)
Smrčka Aleš, Ing., Ph.D. (UITS)
Touili Tayssir, Dr., Ph.D.