TOWARDS AN INTEGRATION OF MESSAGE SEQUENCE CHARTS AND TIMED MAUDE
P. Kosiuczensko, Martin Wirsing · Journal of Integrated Design and Process Science · 2001
This paper is a step toward an integration of a graphical and a formal method and toward building a unifying specification formalism which can support different software views: functional, data, process, and time. In particular, we study the relation of Timed Maude to Message Sequence Charts (MSC). Maude is a formal object-oriented specification language which combines algebraic specification techniques for describing complex data structures with term rewriting to deal with dynamic behav-iour. MSC is a graphical trace language for describing and specifying the communication behaviour of distributed systems by means of message interchange. We show that MSC and Timed Maude fit well together: on one hand, we expand MSC-96 with primitives like multicast, synchronous communica-tion, and multicast, which are available in Maude (these new features will probably appear in MSC-2000). On the other hand, MSC can provide high-level composition mechanisms and a graphical notation for Maude. We expand Timed Simple Maude by two composition operators for sequential and parallel composition. The first one is formalized using a construction analogous to sequencing of automata. The second one is formalized using a syntactic substitution operator derived from a pushout construction. We prove some formal properties like associativity, commutativity and a decomposition property of the second operator.