A semantic and methodological essence of message sequence charts

Message sequence charts (MSCs) are a technique to describe patterns of interaction between the components of interactive distributed systems by specific interaction diagrams. MSCs have evolved in telecommunication applications, defined as a standard, and have become very popular in the design of software architectures and, generally, of distributed or object-oriented software systems. They are used frequently to describe scenarios of interactions illustrating instances of use cases. Nevertheless, both the semantics of MSCs as a technique of specification and their methodological and technical role in the development process have not been precisely and sufficiently clarified, so far. Also their formalization, although tackled by a number of papers, is not well focused with respect to their methodological usage. In this paper, we suggest a semantic model for MSCs in terms of logical propositions characterizing stream-processing functions. This formalization allows us to apply MSCs as an intuitively clear specification technique with a precisely defined meaning. The MSCs provide, in particular, specifications for the components of a system. Our approach is in contrast to other semantic models for MSCs suggested in the literature (see Ladkin, Leue, in: R.L. Tenney et al. (Eds.), Formal Description Techniques VI, North-Holland, 1994, pp. 301–316, and Formal Aspects of Computing 7 (1995) 473–509) where the meaning of MSCs is explained using state transition machines or traces. We define the meaning of MSCs in a more abstract way by a logical technique specifying the components of a system. By this approach MSCs are used for the decomposition of systems into components. Along these lines, we discuss the systematic application of MSCs in the software development process.