Informace o projektu
Automatizovaná verifikace softwaru
- Kód projektu
- GA201/06/1338
- Období řešení
- 1/2006 - 12/2008
- Investor / Programový rámec / typ projektu
-
Grantová agentura ČR
- Standardní projekty
- Fakulta / Pracoviště MU
- Fakulta informatiky
- Klíčová slova
- verifikace, ověřování modelu, software, komponenty
Hlavním cílem projektu je vytvoření teoreticko-metodologického zázemí počítačem podporované a automatické verifikace softwarových systémů. Projekt si klade za úkol podpořit vývoj metodologií, technologií a nástrojů softwarového inženýrství v oblasti technik automatické verifikace. Projekt přispěje k výzkumu směřujícímu k rozvoji poznatků o technologiích pro realistické modelování softwarových systémů, včetně systémů reálného času, specielně s ohledem na bezpečnost jejich provozu. Cílem je navrhnout efektivní implementace těchto modelů a na nich založených metodologiích pro efektivní verifikaci. Projekt se zaměří na zapouzdřené, distribuované a paralelní systémy. Vzhledem k výpočetní náročnosti a rozsáhlosti procesu verifikace je cílem navrhnout metodologie využívající v maximální míře i nové možnosti výpočetních technologií, např. ve smyslu paralelního a distribuovaného počítání v hierarchickém přístupu k paměti.
Výsledky
Hlavním cílem projektu je vytvoření teoreticko-metodologického zázemí počítačem podporované a automatické verifikace softwarových systémů.
Publikace
Počet publikací: 45
2011
-
Flash memory efficient LTL model checking
Science of Computer Programming, rok: 2011, ročník: 76, vydání: 2, DOI
2009
-
Can Flash Memory Help in Model Checking?
Formal Methods for Industrial Critical Systems, rok: 2009
-
Local Quantitative LTL Model Checking
Formal Methods for Industrial Critical Systems, rok: 2009
-
On Decidability of LTL Model Checking for Process Rewrite Systems
Acta informatica, rok: 2009, ročník: 46, vydání: 1
2008
-
Can Flash Memory Help in Model Checking?
13th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2008), rok: 2008
-
Component-Interaction Automata Approach (CoIn)
The Common Component Modeling Example: Comparing Software Component Models, rok: 2008, počet stran: 31 s.
-
DiVinE Cluster
Rok: 2008
-
DiVinE Multi-Core -- A Parallel LTL Model-Checker
Automated Technology for Verification and Analysis, rok: 2008
-
Estimating State Space Parameters
Rok: 2008, druh: Další prezentace na konferencích
-
I/O Efficient Model Checking
Rok: 2008, druh: Další prezentace na konferencích