D 2011

CoInDiVinE: Parallel Distributed Model Checker for Component-Based Systems

BENEŠ, Nikola; Ivana ČERNÁ a Milan KŘIVÁNEK

Základní údaje

Originální název

CoInDiVinE: Parallel Distributed Model Checker for Component-Based Systems

Autoři

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

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"

Odkazy

Označené pro přenos do RIV

Ano

Kód RIV

RIV/00216224:14330/11:00065910

Organizační jednotka

Fakulta informatiky

ISSN

DOI

UT WoS

Klíčová slova anglicky

component-based systems; model checking; parallelization

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 29. 4. 2014 18:20, RNDr. Nikola Beneš, Ph.D.

Anotace

ORIG CZ

V originále

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.

Č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

Přiložené soubory

2011-PDMC.pdf
Požádat o autorskou verzi souboru