Message Sequence Charts and Message Flow Graphs
Publications
-
Stefan Leue: Methods and Semantics for Telecommunications Systems Engineering, Doctoral Dissertation, University of Berne, 1994.
Download: [PDF] [PS]Abstract: 
Not available. -
S. Leue, L. Mehrmann, M. Reza: Synthesizing ROOM Models from Message Sequence Chart Specifications,
13th IEEE Conference on Automated Software Engineering, Honolulu, Hawaii, 1998.
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.
Download: [PDF] [PS] -
H. Ben-Abdallah, S. Leue: MESA: Support for Scenario-Based Design of Concurrent Systems
, Proceedings of the 4th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'98, 1998.
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.
Download: [PDF] [PS] -
Alberto Lluch-Lafuente, Stefan Edelkamp, Stefan Leue: Timing Constraints in Message Sequence Chart Specifications ,
Formal Description Techniques X, Proceedings of the Tenth International Conference on Formal Description Techniques FORTE/PSTV'97, Chapman & Hall, 1997.
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.
Download: [PDF] [PS] -
H. Ben-Abdallah, S. Leue: Expressing and Analyzing Timing Constraints in Message Sequence Chart Specifications
, Technical Report 97-04, Dept. of Electrical and Computer Engineering, University of Waterloo, 1997.
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.
Download: [PDF] [PS] -
H. Ben-Abdallah, S. Leue: Syntactic Detection of Process Divergence and non-Local Choice in Message Sequence Charts
, Proceedings of the Third International Workshop on Tools and Algorithms for the Construction and Analysis of Systems TACAS'97, 1997.
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.
Download: [PDF] [PS] -
H. Ben-Abdallah, S. Leue: Syntactic Analysis of Message Sequence Chart Specifications
, Technical Report 96-12, Dept. of Electrical and Computer Engineering, University of Waterloo, 1996.
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.
Download: [PDF] [PS] -
H. Ben-Abdallah, S. Leue: Architecture of a Requirements and Design Tool Based on Message Sequence Charts
, Technical Report 96-13, Dept. of Electrical and Computer Engineering, University of Waterloo, 1996.
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.
Download: [PDF] [PS] -
S. Leue, P.B. Ladkin: Implementing and Verifying Scenario-Based Specifications Using Promela/XSpin
, Participants Proc. of the Second SPIN Workshop, Rutgers University, New Brunswick, New Jersey, 1996.
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 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 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.
Download: [PDF] [PS] -
P.B. Ladkin, S.Leue: Interpreting Message Flow Graphs
, Pages 473 - 509, Formal Aspects of Computing 7(5), 1995.
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.
Download: [PDF] [PS] -
S.Leue, P.B. Ladkin: Implementing Message Sequence Charts in Promela
, Proc. of the First SPIN Workshop, Proc. of the First SPIN Workshop, Montreal, Canada, 1995.
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.
Download: [PDF] [PS] -
P.B. Ladkin and S.Leue: Comments on a Proposed Semantics for Basic Message Sequence Charts
, The Computer Journal 37 (9), 1995.
Abstract: Comments on a Proposed Semantics for Basic Message Sequence Charts, The Computer Journal, 37(9), January 1995.
Download: [PDF] [PS] -
P.B. Ladkin and S.Leue: Four Issues Concerning the Semantics of Message Flow Graphs
, Formal Description Techniques VII, Proc. of the Seventh IFIP International Conference on Formal Description Techniques FORTE'94, Chapman & Hall, 1995.
Abstract: We discuss four issues concerning the semantics of Message Flow Graphs (MFGs). MFGs are extensively used as pictures of message-passing behavior. One type of MFG, Message Sequence Chart (MSC) is ITU Standard Z.120. We require that a system described by an MFG has global states with respect to its message-passing behavior, with transitions between these states effected by atomic message-passing actions. Under this assumption, we argue (a) that the collection of global message states defined by an MFG is finite (whether for synchronous, asynchronous, or partially-asynchronous message-passing); (b) that the unrestricted use of `conditions' requires processes to keep control history variables of potentially unbounded size; (c) that allowing `crossing' messages of the same type implies certain properties of the environment that are neither explicit nor desirable, and (d) that liveness properties of MFGs are more easily expressed by temporal logic formulas over the control states than by B\"uchi acceptance conditions over the same set of states.
Download: [PDF] [PS] -
S. Leue: QoS Specification Based on SDL /MSC and Temporal Logic
, Proceedings of the Montreal Workshop on Multimedia Applications and Quality of Service Verification, Workshop on Multimedia Applications and Quality of Service Verification, Montreal, 1994.
Abstract: Many telecommunications systems engineers find it convenient to specify functional properties of their systems using state-transition based formal description techniques like SDL or Message Sequence Charts (MSCs). However, the expressiveness of these techniques does not capture Quality of Service (QoS) or Network Performance (Np) requirements because many of these on real-time bounds and probability constraints which these FDTs do not allow to express. However, suitably extended temporal logics allow for a description of these requirements. We introduce a method for the integration of functional system specifications given in SDL or MSC with temporal logic based specifications of QoS or Np requirements. We show how SDL and MSC specifications fit together with Temporal Logic specifications. Then we give examples of delay bound, delay jitter, isochronicity, stochastic reliability and stochastic delay bound constraint specifications. We discuss how our method helps in the specification of Np/QoS mapping problems, of QoS negotiation mechanisms, and of QoS monitoring. Finally we hint at methods for the formal verification of QoS and Np specifications.
Download: [PDF] [PS] -
P.B. Ladkin and S.Leue: What Do Message Sequence Charts Mean?
, Pages 301 - 316, Formal Description Techniques VI, IFIP Transactions C, Proc. of the 6th International Conference on Formal Description Techniques, 1994.
Abstract: We propose a semantics for Message Sequence Charts (MSCs). Our requirements are: to determine unambiguously which execution traces are allowed by an MSC; and to use a finite-state interpretation. Our semantics handles both synchronous and asynchronous communication. We define a global state automaton from an MSC, by first defining a transition system of global states, and from that a B\"uchi automaton. In using MSCs, properties of the environment and liveness properties of the MSC itself may be underspecified. We propose a method using temporal logic formulas to specify the required liveness properties.
Download: [PDF] [PS]