License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/DROPS.MEMICS.2009.2354
URN: urn:nbn:de:0030-drops-23549
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2009/2354/
Go to the corresponding OASIcs Volume Portal

Beneš, Nikola ; Křivánek, Milan ; Štefaňák, Filip

Space Effective Model Checking for Component-Interaction Automata

pdf-format:
09006.BenesNikola.2354.pdf (0.3 MB)

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.

BibTeX - Entry

@InProceedings{bene_et_al:OASIcs:2009:2354,
  author =	{Nikola Bene{\v{s}} and Milan Křiv{\'a}nek and Filip {\v{S}}tefaň{\'a}k},
  title =	{{Space Effective Model Checking for Component-Interaction Automata}},
  booktitle =	{Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09)},
  pages =	{78--85},
  series =	{OpenAccess Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-15-6},
  ISSN =	{2190-6807},
  year =	{2009},
  volume =	{13},
  editor =	{Petr Hlinen{\'y} and V{\'a}clav Maty{\'a}{\v{s}} and Tom{\'a}{\v{s}} Vojnar},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2009/2354},
  URN =		{urn:nbn:de:0030-drops-23549},
  doi =		{10.4230/DROPS.MEMICS.2009.2354},
  annote =	{Keywords: Model checking, component-based systems, partial order reduction}
}

Keywords: Model checking, component-based systems, partial order reduction
Collection: Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09)
Issue Date: 2009
Date of publication: 15.12.2009

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI