A semantic and methodological essence of message sequence charts

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.