S Akshay, M Mukund and K Narayan Kumar

*Proc. CONCUR 2007*, Springer LNCS 4703 (2007), 181-196.

*© Springer-Verlag Berlin Heidelberg*

We consider message sequence charts enriched with timing
constraints between pairs of events. As in the untimed
setting, an infinite family of time-constrained message
sequence charts (TC-MSCs) is generated using an HMSC---a
finite-state automaton whose nodes are labelled by TC-MSCs.
A timed MSC is an MSC in which each event is assigned an
explicit time-stamp. A timed MSC *covers* a TC-MSC if
it satisfies all the time constraints of the TC-MSC. A
natural recognizer for timed MSCs is a message-passing
automaton (MPA) augmented with clocks. The question we
address is the following: given a timed system specified as a
time-constrained HMSC *H* and an implementation in the
form of a timed MPA *A*, is every TC-MSC generated by
*H* covered by some timed MSC recognized by
*A*? We give a complete solution for locally
synchronized time-constrained HMSCs, whose underlying
behaviour is always regular. We also describe a restricted
solution for the general case.

- Download PDF.