CoInDiVinE: Parallel Distributed Model Checker for Component-Based Systems

BENEŠ, Nikola, Ivana ČERNÁ a Milan KŘIVÁNEK. CoInDiVinE: Parallel Distributed Model Checker for Component-Based Systems. In Jiří Barnat and Keijo Heljanko. Proceedings 10th International Workshop on Parallel and Distributed Methods in verifiCation. Neuveden: Open Publishing Association, 2011. s. 63-67. ISSN 2075-2180. doi:10.4204/EPTCS.72.

Základní údaje

• Originální název: CoInDiVinE: Parallel Distributed Model Checker for Component-Based Systems
• Autoři: BENEŠ, Nikola (203 Česká republika, garant, domácí), Ivana ČERNÁ (203 Česká republika, domácí) a Milan KŘIVÁNEK (203 Česká republika, domácí).
• Vydání: Neuveden, Proceedings 10th International Workshop on Parallel and Distributed Methods in verifiCation, od s. 63-67, 5 s. 2011.
• Nakladatel: Open Publishing Association

Další údaje

• Originální jazyk: angličtina
• Typ výsledku: Stať ve sborníku
• Obor: 10201 Computer sciences, information science, bioinformatics
• Stát vydavatele: Spojené státy
• Utajení: není předmětem státního či obchodního tajemství
• Forma vydání: elektronická verze "online"
• WWW: URL
• Kód RIV: RIV/00216224:14330/11:00065910
• Organizační jednotka: Fakulta informatiky
• ISSN: 2075-2180
• Doi: http://dx.doi.org/10.4204/EPTCS.72
• UT WoS: 000219679600001
• Klíčová slova anglicky: component-based systems; model checking; parallelization
• Příznaky: Mezinárodní význam, Recenzováno

Anotace

CoInDiVinE is a tool for parallel distributed model checking of interactions among components in hierarchical component-based systems. The tool extends the DiVinE framework with a new input language (component-interaction automata) and a property specification logic (CI-LTL). As the language differs from the input language of DiVinE, our tool employs a new state space generation algorithm that also supports partial order reduction. Experiments indicate that the tool has good scaling properties when run in parallel setting.

Anotace česky

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í.

Návaznosti

• GAP202/11/0312, projekt VaV: Název: Vývoj a verifikace softwarových komponent v zapouzdřených systémech (Akronym: Components in Embedded Systems)

Investor: Grantová agentura ČR, Software Components in Embedded Systems: Development and Verification

• GA201/09/1389, projekt VaV: Název: Verifikace a analýza velmi velkých počítačových systémů

Investor: Grantová agentura ČR, Verifikace a analýza velmi velkých počítačových systémů

• GD102/09/H042, projekt VaV: Název: 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ů

Investor: Grantová agentura ČR, 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ů

• MSM0021622419, záměr: Název: Vysoce paralelní a distribuované výpočetní systémy

Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy

• MUNI/A/0057/2011, interní kód MU: Název: Posílení zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Akronym: SKONF)

Investor: Masarykova univerzita, Posílení zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty