10.4230/LIPICS.FSTTCS.2010.204
Akshay, S.
S.
Akshay
Gastin, Paul
Paul
Gastin
Mukund, Madhavan
Madhavan
Mukund
Narayan Kumar, K.
K.
Narayan Kumar
Model checking time-constrained scenario-based specifications
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
2010
Article
model-checking
message-passing system
time-constrained MSC
Lodaya, Kamal
Kamal
Lodaya
Mahajan, Meena
Meena
Mahajan
2010
2010-12-14
2010-12-14
2010-12-14
en
urn:nbn:de:0030-drops-28649
10.4230/LIPIcs.FSTTCS.2010
978-3-939897-23-1
1868-8969
10.4230/LIPIcs.FSTTCS.2010
LIPIcs, Volume 8, FSTTCS 2010
IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)
2013
8
17
204
215
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Lodaya, Kamal
Kamal
Lodaya
Mahajan, Meena
Meena
Mahajan
1868-8969
Leibniz International Proceedings in Informatics (LIPIcs)
2010
8
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
12 pages
625846 bytes
application/pdf
Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
info:eu-repo/semantics/openAccess
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.
LIPIcs, Vol. 8, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010), pages 204-215