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, Doctor grants
MSM0021622419, plan (intention)Name: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministry of Education, Youth and Sports of the CR, Research Intents
1ET400300504, research and development projectName: Realistická aplikace formálních metod v komponentových systémech
Investor: Academy of Sciences of the Czech Republic, Information society (National programme of research)
Type Name Uploaded/Created by Uploaded/Created Rights
2009-MEMICS.pdf   File version Beneš, N. 14. 12. 2012

Rights

Right to read
 
Right to upload
 
Right to administer:
  • a concrete person Mgr. Milan Křivánek, učo 172831
  • a concrete person Mgr. Filip Štefaňák, učo 256402
  • a concrete person RNDr. Nikola Beneš, Ph.D., učo 72525
Attributes
 
Print
Ask the author for author copy Displayed: 24. 7. 2021 12:46