Message Sequence Charts as a Model of Computation
by
Alexander Letichevsky
Glushkov Institute of Cybernetics, National Academy of Sciences of Ukraine
Coauthors: S.Baranov, J.Kapitonova, V.Kotlyarov

Message Sequence Charts (MSC) are widely used in engineering practice for modeling of distributed interactive systems [1]. The MSC language has simple graphic representation, it is very easy to access and use. Friendly commercial editors and tools for design and verification made this language popular in the engineering community. The standardization of the language caused the interest to formalizing its semantics. The main work for MSC and related language of interworkings was done by M.A.Reniers [2, 3]

Originally MSC was developed for the description of the behavior of systems and semantics of MSC was defined in terms of process algebra (the standard is trace semantics, but bisimilarity can be considered as well). The practical applications of MSC has been required to extend the language introducing some computational features. The extended version mMSC of MSC language has been developed for the description of test generators [4] and successfully used for industrial applications. Another extension was oriented to logical verification of requirements for distributed systems [5]. Formal semantics of timed MSC was defined in [6]. It is based on the model of interaction of agents and environments [7] and used for development of verification procedure for checking time correctness of timed MSC diagrams.

A new model of non-deterministic computations has been developed on a base of this experience. The main semantic object used to define the meaning of MSC diagram is an attributed transition system (transition system with labeled transitions and states). The labels of states are mappings from attributes to their values. The labels of transitions are in- and out- messages exchanged between instances. An algebraic system signature \Omega is used to define functions and predicates on attribute domains. It is a multisorted signature if attributes have different types. Functional constant terms are used as the names of instances and messages.

Syntactic objects are MSC diagrams which use first order logic formulas to label conditions. Attributes are used as the only free variables occurring in these formulas. The meaning of messages is defined by means of the set of basic protocols, simple restricted MSC diagrams with pre- and post-conditions. Each basic protocol is equivalent to temporal logic formula for allx (u --> < P > v), where u and v are first order formulas, P is a finite process. All components of this specification can depend on parameters x=(x₁, ..., x_n), so instances and messages are parameterized. Let some interpretation of a signature \Omega is given. The instances of basic protocols obtained by substituting constants instead of x to the formulas u --> < P > v can be composed using special composition called continuation, and define the transition system called universal protocol. To define continuation basic protocols are represented as predicate transformers.

MSC diagram over the signature \Omega and given set of attributes is called correct relative to a given set of basic protocols if it can be decomposed into correct composition of basic protocols for arbitrary interpretations of a signature \Omega. Exact definitions take into account also the influence of conditions used in MSC diagram and possible initial states. MSC computational model is used for the verification of systems represented in the form of annotated MSC diagrams.

[1] ITU-T, Recommendation Z.120: Message Sequence Chart (MSC), ITU-T, Geneva (1993).

[2] M.A.Reniers. Message Sequence Chart: Syntax and Semantics, . Ph.D. thesis, Eindhoven University of Technology, (1999).

[3] S.Mauw, M.A.Reniers. A Process Algebra for Interworkings. In J.A.Bergstra, A.Ponse, S.A.Smolka (Eds), Handbook of Process Algebra, 1269-1326, 2001.

[4] V.Kotlyarov, V.Sukhomlinov. The input test description language on a base of extended MSC diagrams, Cybernetics and System Analysis to be published

[5] S.N.Baranov, J.V.Kapitonova, V.P.Kotlyarov, A.A.Letichevsky, V.A.Volkov, Requirement Capturing and 3CR Approach, IEEE 26-th Annual International Computer Software and Applications Conference COMPSAC 2002.

[6] A.A. Letichevsky, J.V. Kapitonova, V.P.Kotlyarov, A.A.Letichevsky Jr, V.A.Volkov, Semantics of timed MSC language, Cybernetics and System Analysis (4), 2002.

[7] A.Letichevsky, D.Gilbert. A Model for Interaction of Agents and Environments, In D.Bert, C.Choppy, P.Moses (Eds), Resent Trends in Algebraic Development Techniques, LNCS, (1827), 311-328, 1999.

Date received: March 15, 2003