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.
Other formats:   BibTeX LaTeX RIS
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
Changed by Changed by: RNDr. Nikola Beneš, Ph.D., učo 72525. Changed: 17/12/2010 12:27.
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 projectName: 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 projectName: 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
PrintDisplayed: 3/12/2022 16:37