Research Project:

Software Requirements Engineering and Design based on Message Sequence Charts

Research Partners:

Research Team at Waterloo:

Alumni:

Funding:

Duration:

Research Results

We are developing a tool to support the scenario-based design of concurrent, object-oriented real-time systems based on Message Sequence Charts. We developed algorithms that syntactically analyze ITU-T Z.120 hierarchical MSC specifications with respect to semantic ambiguities like process divergence and non-local branching choices. Further work addresses timing information in MSCs and reconciling the ITU-T Z.120 timer notation with alternative proposed notations. We then suggest extending existing timing consistency analysis algorithms (c.f. Dechter, Meiri and Pearl; Alur, Holzmann and Peled) to branching and iterating Z.120-style MSC specifications. The analysis algorithms are being implemented in the MESA toolset that we are currently developing.

• MESA: Support for Scenario-Based Design of Concurrent Systems
• Timing Constraints in Message Sequence Chart Specifications
• Expressing and Analyzing Timing Constraints in Message Sequence Chart Specifications
• Syntactic Detection of Process Divergence and non-Local Choice in Message Sequence Charts
• Syntactic Analysis of Message Sequence Chart Specifications
• Architecture of a Requirements and Design Tool Based on Message Sequence Charts

• MESA (MSC Editor, Simulator and Analyzer): Currently under design and implementation, will eventually implement \
• syntactic checks for process-divergence, timing consistency,
• various semantics analysis functions, and
• code synthesis (ROOM/UML-RT, SDL, Promela.
Implementation currently in Tcl/Tk and C++ under Solaris, but we intend to eventually migrate to JAVA. For a preliminary description of the tool see our technical report "MESA: Support for Scenario-Based Design of Concurrent Systems". It is planned to make a research version of this tool publicly available once a stable version is available, probably towards the end of 1998. In case you would like to receive a copy, please send us an email: <sleue@swen.uwaterloo.ca>.
• xMSC (implemented by Tuan Ngo): A preliminary editor for basic MSCs and HMSC graphs, checks an MSC specification for non-local choice (for the algorithms see our TACAS'97 paper). Saves MSC specification in internal format, and prints MSCs and HMSC to Postscript file. Implemented in Tcl/Tk and C++ under SunOS. Predecessor of MESA, not publicly available.

Research Outline (Taken from original research proposal):

the question of what Message Sequence Charts (MSCs) inherently express, and what users implicitly assume them to express;

the syntactic analysis of MSC specifications in order to detect ambiguities and aspects of underspecification;

possibilities for extensions to notation to make implicit semantics assumptions explicit;

the introduction of composition and refinement/abstraction concepts;

the synthesis of executable processes and related validation and verification concepts (e.g., model checking of MSC specifications);

the usage of MSCs as `constraints'; and

the incorporation of real-time requirements and object-orientation concepts into the language.