18th International Conference on Concurrency Theory

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.

• Type: Journal
• Year: 2010
• Where: IANDC
• Authors: Luís Caires, Vasco Thudichum Vasconcelos
• Keywords: Business, IANDC 2010, Message Sequence Charts, Time-constrained Hmscs, Timed Msc