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
2007
-
DiVinE Multi-Core
Rok: 2007
-
I/O Efficient Accepting Cycle Detection
19th International Conference on Computer Aided Verification, rok: 2007
-
Model Checking Large Finite-State Systems and Beyond
33rd Conference on Current Trends in Theory and Practice of Computer Science, rok: 2007
-
Parallel Algorithms for Finding SCCs in Implicitly Given Graphs
Formal Methods: Applications and Technology, rok: 2007
-
Parallel Model Checking and the FMICS-jETI Platform
Proceedings Twelfth IEEE International Conference on Engineering of Complex Computer Systems, rok: 2007
-
ProbDiVinE
Rok: 2007
-
Relaxed Cycle Condition Improves Partial Order Reduction
3rd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2007), rok: 2007
-
Scalable Multi-core LTL Model-Checking
Model Checking Software, rok: 2007
-
Tutorial: Parallel Model Checking
Model Checking Software, rok: 2007
-
Verifying VHDL Designs with Multiple Clocks in SMV
Formal Methods Applications and Technology, 11th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2006, and 5th International Workshop on Parallel and Distributed Methods in Verification, PDMC 2006, rok: 2007