Informace o projektu
Formální verifikace: algoritmy, vlastnosti modelovacích formalismů a temporálních logik
- Kód projektu
- GP201/08/P375
- Období řešení
- 1/2008 - 12/2010
- Investor / Programový rámec / typ projektu
-
Grantová agentura ČR
- Postdoktorské projekty
- Fakulta / Pracoviště MU
- Fakulta informatiky
- Klíčová slova
- formální verifikace, ověřování modelu, nekonečné systémy, temporální logiky
Procesy ověřování a garance kvality založené převážně na práci lidí nejsou vhodné pro vývoj dnešních rozsáhlých hardwarových a softwarových systémů. A právě výzkum v oblasti automatické formální verifikace je tématem předkládaného projektu. navrhovatel se chce konkrétně zaměřit na tři oblasti:
- vlastnosti temporálních logik a využití těchto vlastností při konstrukci nových a vylepšení stávajících verifikačních algoritmů
- vlastnosti formalismů pro popis nekonečně stavových systémů - jejich vyjadřovací síla a rozhodnutelnost základních verifikačních problémů pro odpovídající třídy nekonečně stavových systémů
- progresivní směry ve verifikaci softwaru - zejména verifikace vlastností souvisejících s dynamicky alokovanou pamětí a aplikace verifikačních technik na běžné programovací jazyky. Výstupem projektu budou publikace v mezinárodních časopisech a na mezinárodních konferencích a workshopech.
Výsledky
Cílem projektu je základní výzkum ve vybraných oblastech automatické formální verifikace a publikace dosažených výsledků na mezinárodní úrovni.
Publikace
Počet publikací: 7
2012
-
Almost linear Büchi automata
Mathematical Structures in Computer Science, rok: 2012, ročník: 22, vydání: 2, DOI
2010
-
Decidable Race Condition and Open Coregions in HMSC
Proceedings of the Ninth International Workshop on Graph Transformation and Visual Modeling Techniques (GT-VMT 2010), rok: 2010
2009
-
Almost Linear Büchi Automata
Proceedings 16th International Workshop on Expressiveness in Concurrency 2009 (EXPRESS'09), rok: 2009
-
On Decidability of LTL Model Checking for Process Rewrite Systems
Acta informatica, rok: 2009, ročník: 46, vydání: 1
-
On Decidability of LTL+Past Model Checking for Process Rewrite Systems
Joint Proceedings of the 8th, 9th, and 10th International Workshops on Verification of Infinite-State Systems (INFINITY 2006, 2007, 2008), rok: 2009
-
Reachability is decidable for weakly extended process rewrite systems
Information and Computation, rok: 2009, ročník: 207, vydání: 6
2008
-
Petri Nets Are Less Expressive Than State-Extended PA
Theoretical Computer Science, rok: 2008, ročník: 394, vydání: 1-2