Techniques avancées pour la vérification de systčmes ŕ nombre d'états infini.

Description in Czech
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.

Keywords
vérification automatique, systmes infinis, model checking

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

MEB 020840

French

Vojnar Tomáš, prof. Ing., Ph.D. - principal person responsible
Bouajjani Ahmed - fellow researcher
Češka Milan, prof. RNDr., CSc. - fellow researcher
Holík Lukáš, doc. Mgr., Ph.D. - fellow researcher
Rogalewicz Adam, doc. Mgr., Ph.D. - fellow researcher
Smrčka Aleš, Ing., Ph.D. - fellow researcher
Touili Tayssir, Dr., Ph.D. - fellow researcher

Department of Intelligent Systems
- responsible department (1.1.1989 - not assigned)
Automated Analysis and Verification Research Group - VeriFIT
- internal (20.2.2008 - 31.12.2009)
Department of Intelligent Systems
- co-beneficiary (20.2.2008 - 31.12.2009)

Responsibility: Vojnar Tomáš, prof. Ing., Ph.D.