Title : Matching scenarios with timing constraints
Authors : Prakash Chandrasekaran, Madhavan Mukund
Abstract:
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.