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
-
Model Checking of RegCTL
Computing and Informatics, rok: 2006, ročník: 25, vydání: 1
-
On Alternative Construction of LTL Tableau
2nd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2006), rok: 2006
-
On Combining Partial Order Reduction with Fairness Assumptions
Proceedings of the 11th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2006), rok: 2006
-
On Decidability of LTL Model Checking for Process Rewrite Systems
FSTTCS 2006: 26th International Conference on Foundations of Software Technology and Theoretical Computer Science, 26th International Conference, Kolkata, India, December 13-15, 2006, Proceedings, rok: 2006
-
On Decidability of LTL Model Checking for Weakly Extended Process Rewrite Systems
Rok: 2006, druh: Prezentace v oblasti VaV (AV tvorba, WEB aplikace apod.)
-
Parallel Algorithms for Finding SCCs in Implicitly Given Graphs
Proceedings of the 5th International Workshop on Proceedings of 5th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2006), rok: 2006
-
Refining Undecidability Border of Weak Bisimilarity.
Proceedings of the 7th International Workshop on Verification of Infinite-State Systems (INFINITY'05), rok: 2006
-
Routing and Level 2 Addressing in a Hardware Accelerator for Network Applications
ICT 2006, 13th International Conference on Telecommunications, rok: 2006
-
Special Issue on Parallel and Distributed Verification - Foreword
Formal Methods in System Design, rok: 2006, ročník: 29, vydání: 2
-
Test Input Generation for Java Containers using State Matching
International Symposium on International Symposium on Software Testing and Analysis, rok: 2006