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
2006
-
Cluster-Based LTL Model Checking of Large Systems
Formal Methods for Components and Objects, rok: 2006
-
Component Substitutability via Equivalencies of Component-Interaction Automata
Pre-proceedings of the International Workshop on Formal Aspects of Component Software (FACS'06), rok: 2006
-
Distributed breadth-first search LTL model checking
Formal Methods in System Design, rok: 2006, ročník: 29, vydání: 2
-
Distributed Qualitative LTL Model Checking of Markov Decision Processes
Proceedings of 5th International Workshop on Parallel and Distributed Methods in verifiCation, rok: 2006
-
Distributed Verification: Exploring the Power of Raw Computing Power
5th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2006), rok: 2006
-
DiVinE -- A Tool for Distributed Verification
Computer Aided Verification, rok: 2006
-
DiVinE Library
Rok: 2006
-
Experimental Comparison of Algorithms Checking Proviso for Partial Order Reduction
2nd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2006), rok: 2006
-
Model Checking of RegCTL
Computing and Informatics, rok: 2006, ročník: 25, vydání: 1
-
On Alternative Construction of LTL Tableau
2nd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2006), rok: 2006