Detail projektu

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

Období řešení: 20.02.2008 — 31.12.2009

O projektu

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

Popis česky
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.

Klíčová slova
vérification automatique, systmes infinis, model checking

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

Označení

MEB 020840

Originální jazyk

francouzština

Řešitelé

Vojnar Tomáš, prof. Ing., Ph.D. - hlavní řešitel
Habermehl Peter - spoluřešitel

Útvary

Ústav inteligentních systémů
- spolupříjemce (20.02.2008 - 31.12.2009)

Výsledky

HABERMEHL, P., RADU, I., VOJNAR, T. A Logic of Singly Indexed Arrays. TR-2008-9, Grenoble: VERIMAG, 2008.
Detail

HOLÍK, L., VOJNAR, T., BOUAJJANI, A., HABERMEHL, P., TOUILI, T. Antichain-based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata. FIT-TR-2008-007, Brno: Faculty of Information Technology BUT, 2008.
Detail

HABERMEHL, P., RADU, I., VOJNAR, T. What else is decidable about integer arrays?. TR-2007-8, Grenoble: VERIMAG, 2008.
Detail