Formal Techniques for Analysing Scenarios using Message Sequence Charts

AbstractThis paper describes light-weight formal techniques based on Message Sequence Charts (MSCs) for capturing and validating early requirements and design. Our focus is on ease of use in specifying, simulating and validating scenarios, and checking their desired properties efficiently. We discuss how the formalism of High Level Message Sequence Charts (HMSCs or MSC'96), can be used to capture scenarios in use cases, thus enabling the use of tools for analysing them. We then present two formal semantics for HMSCs – an intuitive linear time semantics based on runs, and an operational semantics in terms of a labelled transition system. Next we present a way of describing desired properties of use case scenarios using templates, for validating scenarios with respect to informal requirements. The correctness properties of a collection of MSCs can then be established by efficient algorithms for finding paths in a directed graph representing the precedence relation on the events of the MSCs. We have implemented the operational semantics and the verification algorithms in the form of a simulation and verification tool for analysing scenarios