Skip the Organizational structure panel
Organizational structure
On selecting a constituent part of MU the "Overview of publishing activities" page will be displayed with information relevant to the selected constituent part. The "Overview of publishing activities" page is not available for non-activated items.

Masaryk University
- Faculties
- Law
- Medicine
- Science
- Arts
- Education
- Economics
- Informatics
- Social Studies
- Sports Studies
- Institutes
- Computer Science
- CEITEC MU
- Politica
- Specialized Units
- Hostels & Canteens
- University Press
- Telč Centre
- UCB Management
- Rector`s Office
- Rectorate
- Other Units
- Archive
- Language Centre
- International Studies
- Disabled Students
- Technology Transfer
- Biostatistics
- Mendel Museum
- CERIT
- Civic Education
- Project Team CEITEC

Publication details

Space Effective Model Checking for Component-Interaction Automata

Basic information
Original title:	Space Effective Model Checking for Component-Interaction Automata
Authors:	Nikola Beneš, Milan Křivánek, Filip Štefaňák

Further information
Citation:	BENEŠ, Nikola - KŘIVÁNEK, Milan - ŠTEFAŇÁK, Filip. 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. ISBN 978-3-939897-15-6, 8 pp. 2009, Znojmo, Česká republika.
Original language:	English
Field:	Informatika
WWW:	http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=2354
Type:	Article in Proceedings
Keywords:	partial order reduction; model checking; component-based systems

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.

Related projects:

top