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
2007
-
On Decidability of LTL+Past Model Checking for Process Rewrite Systems
Rok: 2007, druh: Další prezentace na konferencích
-
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
-
ProbDiVinE: A Parallel Qualitative LTL Model Checker
Fourth International Conference on the Quantitative Evaluation of Systems (QEST'07), 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
-
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
2006
-
11th International Workshop on Formal Methods for Industrial Critical Systems
Rok: 2006, druh: Uspořádání workshopu
-
Architectural Interoperability Checking in Visual Coordination Networks
Combined Proceedings of the Second International Workshop on Coordination and Organization (CoOrg 2006) and the Second International Workshop on Methods and Tools for Coordinating Concurrent, Distributed and Mobile Systems (MTCoord 2006), rok: 2006