Checking conformance for time-constrained scenario-based specifications

Akshay, S. ; Gastin, Paul ; Mukund, Madhavan ; Narayan Kumar, K. (2015) Checking conformance for time-constrained scenario-based specifications Theoretical Computer Science, 594 . pp. 24-43. ISSN 0304-3975

Full text not available from this repository.

Official URL:

Related URL:


We consider the problem of model checking message-passing systems with real-time requirements. As behavioral 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 behavior can be regarded as a timed automaton. Our goal is to verify that all timed behaviors 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/conformance problem.

Item Type:Article
Source:Copyright of this article belongs to Elsevier Science.
Keywords:MSC Graphs; Timed Automata; Model Checking
ID Code:114102
Deposited On:25 May 2018 04:56
Last Modified:25 May 2018 04:56

Repository Staff Only: item control page