Note:
Postcript
version (242 p.)
No Postscript code available yet.
Abstract:
Message Sequence Chart (MSC) specifications have found their way
into many software engineering methodologies and CASE tools, in particular
in the area of telecommunications and concurrent real-time systems.
MSC Specifications often represent early life-cycle requirements and
high-level design specifications. We are considering iterating and
branching MSC specifications according to ITU-T Recommendation
Z.120. We show how these specifications can be analyzed with respect
to their software architectural content, including structure and
behaviour. We present algorithms for the automated synthesis of
Real-Time Object-Oriented Modeling (ROOM) models from MSC
specifications and discuss their implementation in the Mesa toolset.
The automation of the synthesis contributes to making
the transition from high-level, message exchange-oriented views
to the level of a full life-cycle architecture description more efficient
and
reliable. This means that we are contributing to making Z.120 MSC
specifications more useful in the software engineering process.
Postcript
version (27 p. plus appendix, gzipped, 328 kBytes.)
Postcript
version (27 p. plus appendix, compressed, 601 kBytes.)
Abstract:
The latest ITU-T standard syntax of Message Sequence Charts (MSCs)
offers several operators to compose MSCs in a hierarchical, iterating,
and nondeterministic way. However, current tools operate on MSCs that describe
finite, deterministic behavior. In this paper, we describe the architecture
and the partial implementation of Mesa, an MSC-based tool that supports
early phases of the software development cycle. The main functionalities
of MESA are: an environment for the composition of system models through
MSCs, syntactic and model-based analysis of an MSC model, and resolution
of resource related underspecifications in an MSC model.
Postcript
version (18p., compressed, 503 kBytes.)
A preliminary version of this paper appeared as: Technical Report
97-12, Dept. of Electrical and Computer Engineering, University of
Waterloo, October 1997.
Postcript
version of Technical Report 97-12 (17 p., gzipped, 270 kBytes, inflates
to 7.6 MByte after gzunzip.)
Abstract:
When dealing with timing constraints, the Z.120 standard of Message
Sequence Charts (MSCs) is still evolving along with several proposals.
This paper first reviews proposed extensions of MSCs to describe timing
constraints. Secondly, the paper describes an analysis technique for timing
consistency in iterating and branching MSC specifications. The analysis
extends efficient current techniques for timing analysis of MSCs with no
loops nor branchings. Finally, the paper extends our syntactic analysis
of process divergence to MSCs with timing constraints.
Postcript
version (16 p.)
Abstract:
Message Sequence Charts (MSCs) are increasingly supported in software engineering tools and methodologies for communication systems. The last Z.120 standard extends MSCs with operators to organize them in a compositional, hierarchical fashion to describe systems with non-trivial sizes. When dealing with timing constraints, the standard is still evolving along with several proposals. This paper first reviews proposed extensions of MSCs to describe timing constraints. Secondly, the paper describes an analysis technique for timing consistency in iterating and branching MSC specifications. The analysis extends efficient current techniques for timing analysis of MSCs with no loops or branchings. Finally, we use an example to illustrate our analysis technique.
Postcript
version (28 p.)
Abstract:
Message Sequence Charts (MSCs) are increasingly used in software engineering methodologies and tools to capture, for instance, system requirements, test scenarios, and simulation traces. They have been standardized by ITU-T in Recommendation Z.120~\cite{ITU-T96}. However, various aspects of environment behavior remain underspecified in MSCs, e.g., the presence of resources for inter-process communication and the coordination of concurrent processes at points of control branching. Such underspecifications can result in ambiguities in an MSC specification and discrepancies between an MSC specification and its implementation. In this paper we characterize two consequences of harmful underspecifications: {\em process divergence} and {\em non-local branching choice}. We also present two syntax-based analysis algorithms that detect both problems.
Postcript
version (16 p.)
Abstract:
Message Sequence Charts (MSCs) are gaining popularity in software engineering methods for concurrent and real-time systems. They are increasingly supported in software engineering tools to capture, for instance, system requirements, test scenarios, and simulation traces. MSCs have been standardized by ITU-T in Recommendation Z.120. However, various aspects of environment behavior remain underspecified in MSCs, e.g., the presence of resources for inter-process communication and the coordination of concurrent processes at points of control branching. Such underspecifications can result in ambiguities in an MSC specification and discrepancies between an MSC specification and its implementation. In this paper we characterize two consequences of harmful underspecifications: process divergence and non-local branching choice. We also present two syntax-based analysis algorithms that detect both problems. The syntactic characterization of these problems requires an MSC specification to be deadlock-free. Therefore, we also discuss deadlock detection in MSC specifications.
Postcript
version (39 p.)
Abstract:
Message Sequence Charts (MSCs) are increasingly supported in software engineering tools to capture system requirements, test scenarios, and simulation traces of reactive systems. The latest standard syntax of MSCs offers operations to compose MSCs in a hierarchical, iterating, and nondeterministic way. The various operators are a step towards increasing the applicability of MSCs to more than a trace language. However, current tools operate on MSCs that describe finite, deterministic behavior and none of them uses MSCs as a language for requirements specification and design of a system. In this paper, we propose an architecture for an MSC-based tool to support the requirements specification and design phases. The main functionalities of the tool are: an environment for the composition of system models through MSCs, syntactic and model-based analysis of an MSC model, and resolving resource related underspecifications in an MSC model. The proposed tool also supports synthesis mechanisms as a means to integrate our tool with available tools, e.g., the SPIN model-checker. In this paper, we also review the theoretical results we have currently developed towards realizing the proposed tool.
Postcript
version (19 p.)
Abstract:
We discuss a translation of Message Sequence Charts (MSCs) into the language PROMELA (we call this translation an `{\em implementation}') that is consistent with the formal semantics we have previously defined for Message Flow Graphs and Message Sequence Charts, which handled the syntactic features with mathematical import from ITU-T recommendation Z.120. We report on experiments executing the PROMELA code using the XSPIN simulator and validator. In previous work we found that potential process {\em divergence} and {\em non-local choice} situations impose problems on implementations of MSCs, and we discuss how these impact our PROMELA translation and suggest solutions. Finally, we show how to model-check liveness requirements imposed on MSC specifications. We use the PROMELA models obtained from our implementation, describe how to use control state propositions based on these models, use Linear Time Temporal Logic formulas to specify the liveness properties, and demonstrate the use of XSPIN as a model checker for these properties.
PostScript
version (23 p.)
Abstract:
In previous work we defined a finite state semantics for Message Sequence Charts (MSCs) and suggested a translation of MSC specifications into Promela. We call this translation an `{\em implementation}'. In this paper we reconsider the implementation of MSCs and discuss what information needs to be added when implementing MSC specifications containing so-called {\em non-local choices}. Next, we show how to model-check liveness requirements imposed on MSC specifications. We use the Promela models obtained from our implementation, describe how to use control state propositions based on these models, use Linear Time Temporal Logic formulas to specify the liveness properties, and demonstrate the use of XSpin as a model checker for these properties.
PostScript
version (18 p.)
Abstract:
We give a semantics for Message Flow Graphs (MFGs), which play the role for interprocess communication that Program Dependence Graphs play for control flow in parallel processes. MFGs have been used to analyse parallel code, and are closely related to Message Sequence Charts and Time Sequence Diagrams in telecommunications systems. Our requirements are firstly, to determine unambiguously exactly what execution traces are specified by an MFG, and secondly, to use a finite-state interpretation. Our methods function for both asynchronous and synchronous communications. From a set of MFGs, we define a transition system of global states, and from that a B\"uchi automaton by considering safety and liveness properties of the system. In order easily to describe liveness properties, we interpret the traces of the transition system as a model of Manna-Pnueli temporal logic. Finally, we describe the expressive power of MFGs by mimicking an arbitrary B\"uchi automaton by means of a set of MFGs.
PostScript
version (37 p.)
Abstract:
We have previously defined a formal semantics for Message Flow Graphs and Message Sequence Charts, capturing most of the syntactic features contained in ITU-T recommendation Z.120. We discuss here a translation of MSCs into the language {\em Promela}, and report on experiments executing the Promela code using the {\em SPIN} simulator and validator.
PostScript
version (3 p.)