Scenario-based specifications such as message sequence charts (MSC) offfer an intuitive and visual way of describing design requirements. Such specifications focus on message exchanges among communicating entities in distributed software systems. Structured specifications such as MSC-traphs and Hierarchical MSC-graphs (HMSC) allow convenient expression of multiple scenarios, and can be viewed as an early model of the system. In this paper, we present a comprehensive study of the problem of verifying whether this model satisfies a temporal requirement given by an automaton, by developing algorithms for the different cases along with matching lower bounds.
展开▼
