Informace o projektu
Automatická analýza modelů pomocí procházení stavového prostoru
- Kód projektu
- GP201/07/P035
- Období řešení
- 1/2007 - 12/2009
- Investor / Programový rámec / typ projektu
-
Grantová agentura ČR
- Postdoktorské projekty
- Fakulta / Pracoviště MU
- Fakulta informatiky
- Klíčová slova
- modelování, simulace, verifikace, stavový prostor
Projekt se zabývá třemi typy modelovacích formalismů: rozšířenými konečnými automaty, systémovými modely a modely založenými na agentech. Aplikace těchto modelů sahají od návrhu a verifikace počítačových systémů až po studium komplexních systémů. Tématem projekt je automatická analýza těchto modelů technikou procházení stavového prostoru. Tento typ analýzy poskytuje bohatší informace o modelu než simulace, která je pro analýzu běžně používána. Projekt se zaměřuje na studium prakticky používaných modelů, na návrh a evaluaci nových technik a ana syntézu a přenos technik vyvinutých v různých aplikačních doménách.
Výsledky
Cílem projektu je vytvořit databázi modelů a zkoumat vlastnosti jejich stavových prostorů, vyvíjet nové techniky analýzy založené na procházení stavových prostorů, implementovat je a experimentálně vyhodnocovat. Výstupy projektu budou veřejně dostupné pomocí internetového portálu projektu.
Publikace
Počet publikací: 8
2009
-
EMMA: Explicit Model Checking Manager (Tool Presentation)
Model Checking Software, rok: 2009
2008
-
Complementarity of Error Detection Techniques
Parallel and Distributed Methods in verifiCation (PDMC 2008), rok: 2008
-
Estimating State Space Parameters
Rok: 2008, druh: Další prezentace na konferencích
-
Fighting State Space Explosion: Review and Evaluation
Formal Methods for Industrial Critical Systems, rok: 2008
-
Model Classifications and Automated Verification
Formal Methods for Industrial Critical Systems, rok: 2008
-
Properties of State Spaces and Their Applications
International Journal on Software Tools for Technology Transfer (STTT), rok: 2008, ročník: 10, vydání: 5
2007
-
BEEM: Benchmarks for Explicit Model Checkers
Model Checking Software, rok: 2007
-
Predicate Abstraction with Under-Approximation Refinement
Logical Methods in Computer Science, rok: 2007, ročník: 3, vydání: 1