Verifying compositional designs for scenario-based timing specifications

In this paper, we use networks of UML statechart diagrams to model compositional designs for real-time systems, and present an algorithm for checking networks of statechart diagrams for the scenario-based specifications expressed by UML sequence diagrams with timing constraints. The algorithm is based on investigating the reachability graph of the integer state space of a network of statechart diagrams