Space Effective Model Checking for Component-Interaction Automata

BENEŠ, Nikola, Milan KŘIVÁNEK and Filip ŠTEFAŇÁK. Space Effective Model Checking for Component-Interaction Automata. In Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09). Dagstuhl, Německo: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, Německo, 2009. 8 pp. ISBN 978-3-939897-15-6.

Basic information

• Original name: Space Effective Model Checking for Component-Interaction Automata
• Name in Czech: Prostorově efektivní ověřování modelu pro komponentově-interakční automaty
• Authors: BENEŠ, Nikola (203 Czech Republic, guarantor, belonging to the institution), Milan KŘIVÁNEK (203 Czech Republic, belonging to the institution) and Filip ŠTEFAŇÁK (703 Slovakia, belonging to the institution).
• Edition: Dagstuhl, Německo, Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09), 8 pp. 2009.
• Publisher: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, Německo

Other information

• Original language: English
• Type of outcome: Proceedings paper
• Field of Study: 10201 Computer sciences, information science, bioinformatics
• Country of publisher: Germany
• Confidentiality degree: is not subject to a state or trade secret
• WWW: URL
• RIV identification code: RIV/00216224:14330/09:00028809
• Organization unit: Faculty of Informatics
• ISBN: 978-3-939897-15-6
• Keywords (in Czech): redukce pomocí reprezentantů; ověřování modelu; komponentové systémy
• Keywords in English: partial order reduction; model checking; component-based systems
• Tags: Component-based systems, Component-Interaction automata, Model checking, partial order reduction, verification

Abstract

The techniques of component-based development are becoming a common practice in the area of software engineering. One of the crucial issues in the correctness of such systems is the correct interaction among the components. The formalism of component-interaction automata was devised to model various aspects of such interaction, as well as to allow automated verification in the form of model checking with properties expressed in the component-interaction LTL, a variant of the known linear temporal logic. As the state space of a component-based system can grow exponentially with the number of components, it is desirable to employ reduction techniques to make the verification task more feasible. In our work, we describe the implementation of the ample set partial order reduction method within the component-interaction automata verification framework. Due to the state and action-based nature of both the modelling and specification formalisms, the implementation differs from traditional state-based approaches. After describing the implementation, we present some of the results obtained by employing the enhanced verification framework on a case study.

Links

• GD102/09/H042, research and development project: Name: 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: Czech Science Foundation

• MSM0021622419, plan (intention): Name: Vysoce paralelní a distribuované výpočetní systémy

Investor: Ministry of Education, Youth and Sports of the CR, Highly Parallel and Distributed Computing Systems

• 1ET400300504, research and development project: Name: Realistická aplikace formálních metod v komponentových systémech

Investor: Academy of Sciences of the Czech Republic, Realistic application of formal methods in component systems