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
2008
-
A Case Study in Parallel Verification of Component-Based Systems
Pre-proceedings of the Workshop on Parallel and Distributed Methods in verifiCation (PDMC'08), rok: 2008
-
Automated Computing of the Maximal Number of Handled Clients for Client-Server Systems
Proceedings of the International Workshop on Formal Aspects of Component Software (FACS'08), rok: 2008
-
Can Flash Memory Help in Model Checking?
13th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2008), rok: 2008
-
Component-Interaction Automata Approach (CoIn)
The Common Component Modeling Example: Comparing Software Component Models, rok: 2008, počet stran: 31 s.
-
DiVinE Cluster
Rok: 2008
-
DiVinE Multi-Core -- A Parallel LTL Model-Checker
Automated Technology for Verification and Analysis, rok: 2008
-
Estimating State Space Parameters
Rok: 2008, druh: Další prezentace na konferencích
-
Formal verification of systems with an unlimited number of components
IET Software journal, rok: 2008, ročník: Volume 2, vydání: Isuue 6
-
From Simple Regulatory Motifs to Parallel Model Checking of Complex Transcriptional Networks
Proceedings of PDMC 2008 - Parallel and Distributed Methods ins VerifiCation, rok: 2008
-
I/O Efficient Model Checking
Rok: 2008, druh: Další prezentace na konferencích