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
2006
-
Weakly Extended Process Rewrite Systems
Rok: 2006, druh: Další prezentace na konferencích
2005
-
Concrete Search with Abstract Matching and Refinement
Computer Aided Verification, rok: 2005
-
CRC64 Algorithm Analysis and Verification
Rok: 2005, druh: Prezentace v oblasti VaV (AV tvorba, WEB aplikace apod.)
-
Distributed Analysis of Large Systems
Formal Methods for Components and Objects, rok: 2005
-
DIVINE - The Distributed Verification Environment
In proceedings of 4th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC05), rok: 2005
-
DivSPIN - A SPIN compatible distributed model checker
Proceedings of 4th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC05), rok: 2005
-
Enhancing Random Walk State Space Exploration
Formal Methods for Industrial Critical Systems, rok: 2005
-
How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors
Proceedings of the 4th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2005), rok: 2005
-
MTCoord 2005 1st International Workshop on Methods and Tools for Coordinating Concurrent, Distributed and Mobile Systems
Rok: 2005, druh: Uspořádání workshopu
-
On Sampled Semantics of Timed Systems
Foundations of Software Technology and Theoretical Computer Science, rok: 2005