Informace o projektu
Techniky automatické verifikace a validace softwarových a hardwarových systémů
- Kód projektu
- 1ET408050503
- Období řešení
- 1/2005 - 12/2009
- Investor / Programový rámec / typ projektu
-
Akademie věd ČR
- Informační společnost (Národní program výzkumu)
- Fakulta / Pracoviště MU
- Fakulta informatiky
- Klíčová slova
- Počítačem podporovaná a automatická verifikace, teorie a technologie modelování rozsáhlých systémů, metodologie softwarového inženýrství, zapouzdřené komponenty, paralelní a distribuované systémy, systémy reálného času
Hlavním cílem projektu je vytvoření teoreticko-metodologického zázemí počítačem podporované a automatické verifikace rozsáhlých softwarových a hardwarový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í rozsáhlých systémů, včetně systémů reálného času a pravděpodobnostních systémů, 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čítaní a v hierarchickém přístupu k paměti.
Výsledky
Teoreticko-metodologické zázemí modelování rozsáhlých systémů. Návrh, analýza a implementace technik pro počítačem podporovanou i automatickou verifikaci a validaci systémů se zaměřením na zapouzdřené, paralelní a distribuované komponenty.
Publikace
Počet publikací: 94
2009
-
CUDA Accelerated LTL Model Checking
Proceedings of the 15th International Conference on Parallel and Distributed Systems, rok: 2009
-
DiVinE 2.0
Rok: 2009
-
DiVinE 2.0: High-Performance Model Checking
International Workshop on High Performance Computational Systems Biology, rok: 2009
-
DiVinE Cuda
Rok: 2009
-
DiVinE-CUDA - A Tool for GPU Accelerated LTL Model Checking
Electronic Proceedings in Theoretical Computer Science, rok: 2009, ročník: 14, vydání: Prosinec
-
Checking Thorough Refinement on Modal Transition Systems Is EXPTIME-Complete
Theoretical Aspects of Computing - ICTAC 2009, 6th International Colloquium, Kuala Lumpur, Malaysia, August 16-20, 2009. Proceedings, rok: 2009
-
Local Quantitative LTL Model Checking
Formal Methods for Industrial Critical Systems, rok: 2009
-
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
-
Partial Order Reduction for State/Event LTL
Proceedings of the International Conference on Integrated Formal Methods (IFM'09), rok: 2009
-
Reachability is decidable for weakly extended process rewrite systems
Information and Computation, rok: 2009, ročník: 207, vydání: 6