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
2012
-
On-the-fly Parallel Model Checking Algorithm that is Optimal for Verification of Weak LTL Properties
Science of Computer Programming, rok: 2012, ročník: 77, vydání: 12, DOI
2011
-
Distributed Algorithms for SCC Decomposition
Journal of Logic and Computation, rok: 2011, ročník: 21, vydání: 1, DOI
-
Flash memory efficient LTL model checking
Science of Computer Programming, rok: 2011, ročník: 76, vydání: 2, DOI
2010
-
Scalable shared memory LTL model checking
International Journal on Software Tools for Technology Transfer (STTT), rok: 2010, ročník: 12, vydání: 2, DOI
2009
-
A Time-Optimal On-the-Fly Parallel Algorithm for Model Checking of Weak LTL Properties
Formal Methods and Software Engineering, rok: 2009
-
BioDiVinE: A Framework for Parallel Analysis of Biological Models
Proceedings of 2nd International Workshop on Computational Models for Cell Processes, rok: 2009
-
BioDiVinE: A Tool for Parallel Analysis of Multi-Affine ODE Models
Computational Mehotds in Systems Biology: Abstract of the Posters, rok: 2009
-
Can Flash Memory Help in Model Checking?
Formal Methods for Industrial Critical Systems, rok: 2009
-
Cluster-Based I/O-Efficient LTL Model Checking
24th IEEE/ACM International Conference on Automated Software Engineering, rok: 2009
-
Computational Analysis of Large-Scale Multi-Affine ODE Models
International Workshop on High Performance Computational Systems Biology, rok: 2009