CoInDiVinE: Parallel Distributed Model Checker for Component-Based Systems

• Autoři: BENEŠ Nikola; ČERNÁ Ivana; KŘIVÁNEK Milan
• Rok publikování: 2011
• Druh: Článek ve sborníku
• Konference: Proceedings 10th International Workshop on Parallel and Distributed Methods in verifiCation
• Fakulta / Pracoviště MU: Fakulta informatiky
• www: http://eptcs.org/paper.cgi?PDMC2011.7
• Doi: http://dx.doi.org/10.4204/EPTCS.72
• Obor: Informatika
• Klíčová slova: component-based systems; model checking; parallelization

Přiložené soubory

• 2011-PDMC.pdf

• Popis: CoInDiVinE je nástroj pro paralelní distribouvané ověřování modelů zachycujících interakce mezi komponentami v hierarchických komponentových systémech. Tento nástroj rozšiřuje existující nástroj DiVinE o nový vstupní jazyk (automaty komponentové interakce) a logiku pro specifikaci vlastností (CI-LTL). Protože nový vstupní jazyk je odlišný od standardního jazyka nástroje DiVinE, bylo třeba pro něj vytvořit nový algoritmus prohledávání stavového prostoru, který podporuje techniku redukce pomocí částečného uspořádání. Experimenty ukazují, že náš nástroj má dobré škálovací vlastnosti při použití v paralelním prostředí.

Související projekty

• Vysoce paralelní a distribuované výpočetní systémy
• Verifikace a analýza velmi velkých počítačových systémů
• Matematické a inženýrské metody pro vývoj spolehlivých a bezpečných paralelních a distribuovaných počítačových systémů
• Software Components in Embedded Systems: Development and Verification
• Posílení zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity