Checking coverage for infinite collections of timed scenarios

Akshay, S. ; Mukund, Madhavan ; Narayan Kumar, K. (2007) Checking coverage for infinite collections of timed scenarios In: 18th International Conference on Concurrency Theory, CONCUR 2007, 03-08 Sep 2007, Lisbon, Portugal.

Full text not available from this repository.

Official URL:

Related URL:


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 А, is every TC-MSC generated by H covered by some timed MSC recognized by А? 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.

Item Type:Conference or Workshop Item (Paper)
Source:Copyright of this article belongs to Springer-Verlag.
ID Code:114145
Deposited On:25 May 2018 04:55
Last Modified:25 May 2018 04:55

Repository Staff Only: item control page