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
2008
-
Improved Distributed Algorithms for SCC Decomposition
Electronic Notes in Theoretical Computer Science, rok: 2008, ročník: 2008, vydání: 198(1)
-
Petri Nets Are Less Expressive Than State-Extended PA
Theoretical Computer Science, rok: 2008, ročník: 394, vydání: 1-2
-
ProbDiVinE-MC
Rok: 2008
-
ProbDiVinE-MC: Multi-core LTL Model Checker for Probabilistic Systems
QEST '08: Proceedings of the 2008 Fifth International Conference on Quantitative Evaluation of Systems, rok: 2008
-
Revisiting Resistance Speeds Up I/O Efficient LTL Model Checking
Tools and Algorithms for the Construction and Analysis of Systems, rok: 2008
-
Semi-external LTL Model Checking
20th International Conference on Computer Aided Verification, rok: 2008
-
Semi-External LTL Model Checking
Rok: 2008, druh: Konferenční abstrakty
-
Shared Hash Tables in Parallel Model Checking
Electronic Notes in Theoretical Computer Science, rok: 2008, ročník: 2008, vydání: 198(1)
-
Squeeze All the Power Out of Your Hardware to Verify Your Software!
Leveraging Applications of Formal Methods, Verification and Validation, rok: 2008
2007
-
Component Substitutability via Equivalencies of Component-Interaction Automata
Electronic Notes in Theoretical Computer Science, rok: 2007, ročník: 182, vydání: 1