Matching scenarios with timing constraints

Networks of communicating finite-state machines equipped with local clocks generate timed MSCs. We consider the problem of checking whether these timed MSCs are “consistent” with those provided in a timed MSC specification. In general, the specification may be both positive and negative. The system should execute all positive scenarios “sensibly”. On the other hand, negative scenarios rule out some behaviours as illegal. This is more complicated than the corresponding problem in the untimed case because even a single timed MSC specification implicitly describes an infinite family of timed scenarios. We outline an approach to solve this problem that can be automated using Uppaal