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/LIPIcs.FSTTCS.2010.204
URN: urn:nbn:de:0030-drops-28649
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2010/2864/
Go to the corresponding LIPIcs Volume Portal

Akshay, S. ; Gastin, Paul ; Mukund, Madhavan ; Narayan Kumar, K.

Model checking time-constrained scenario-based specifications

pdf-format:
18.pdf (0.6 MB)

Abstract

We consider the problem of model checking message-passing systems with real-time requirements. As behavioural specifications, we use message sequence charts (MSCs) annotated with timing constraints. Our system model is a network of communicating finite state machines with local clocks, whose global behaviour can be regarded as a timed automaton. Our goal is to verify that all timed behaviours exhibited by the system conform to the timing constraints imposed by the specification. In general, this corresponds to checking inclusion for timed languages, which is an undecidable problem even for timed regular languages. However, we show that we can translate regular collections of time-constrained MSCs into a special class of event-clock automata that can be determinized and complemented, thus permitting an algorithmic solution to the model checking problem.

BibTeX - Entry

@InProceedings{akshay_et_al:LIPIcs:2010:2864,
  author =	{S. Akshay and Paul Gastin and Madhavan Mukund and K. Narayan Kumar},
  title =	{{Model checking time-constrained scenario-based specifications}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)},
  pages =	{204--215},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-23-1},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{8},
  editor =	{Kamal Lodaya and Meena Mahajan},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2010/2864},
  URN =		{urn:nbn:de:0030-drops-28649},
  doi =		{10.4230/LIPIcs.FSTTCS.2010.204},
  annote =	{Keywords: model-checking, message-passing system, time-constrained MSC}
}

Keywords: model-checking, message-passing system, time-constrained MSC
Collection: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)
Issue Date: 2010
Date of publication: 14.12.2010

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