Generating Timed Scenarios from Behaviours

We study the problem of generating timed scenarios from finite sets of behaviours. We present a new method that, given a finite set of behaviours, constructs a timed scenario whose semantics includes all the behaviours in the set. Moreover, the constructed scenario is subsumed by any other scenario whose semantics includes the given set of behaviours. The method is particularly useful when there is no formal specification for the system (or for part of the system) that is being modelled. In that case our approach serves as a practical method of constructing a formal specification of a system, in the form of a timed scenario. Our experiments show some quantitative results that throw light on the practicability of synthesizing specifications solely from the observed (or expected) behaviours of a system.