TOWARDS AN INTEGRATION OFMESSAGE SEQUENCE CHARTS ANDTIMED MAUDE

摘要

This paper is a step toward an integration of a graphical and a formal method and toward building arnunifying specification formalism which can support different software views: functional, data, process,rnand time. In particular, we study the relation of Timed Maude to Message Sequence Charts (MSC).rnMaude is a formal object-oriented specification language which combines algebraic specificationrntechniques for describing complex data structures with term rewriting to deal with dynamic behaviour.rnMSC is a graphical trace language for describing and specifying the communication behaviourrnof distributed systems by means of message interchange. We show that MSC and Timed Maude fit wellrntogether: on one hand, we expand MSC-96 with primitives like multicast, synchronous communication,rnand multicast, which are available in Maude (these new features will probably appear in MSC-rn2000). On the other hand, MSC can provide high-level composition mechanisms and a graphicalrnnotation for Maude. We expand Timed Simple Maude by two composition operators for sequentialrnand parallel composition. The first one is formalized using a construction analogous to sequencing ofrnautomata. The second one is formalized using a syntactic substitution operator derived from arnpushout construction. We prove some formal properties like associativity, commutativity and arndecomposition property of the second operator.