Model Checking Time-Constrained Scenario-Based Specifications
The authors consider the problem of model checking message-passing systems with real-time requirements. As behavioural specifications, they use Message Sequence Charts (MSCs) annotated with timing constraints. Their system model is a network of communicating finite state machines with local clocks, whose global behaviour can be regarded as a timed automaton. Their 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.