Abstract
Message sequence charts (MSCs) is a standard notation for describing the interaction between communicating objects. It is popular among the designers of communication protocols. MSCs enjoy both a visual and a textual representation. High level MSCs (HMSCs) allow specifying infinite scenarios and different choices. Specifically, an HMSC consists of a graph, where each node is a finite MSC with matched send and receive events, and vice versa. In this paper we demonstrate a weakness of HMSCs, which disallows one to model certain interactions. We will show, by means of an example, that some simple finite state and simple communication protocol cannot be represented using HMSCs. We then propose an extension to the MSC standard, which allows HMSC nodes to include unmatched messages. The corresponding graph notation will be called HCMSC, which stands for High level Compositional Message Sequence Charts. With the extended framework, we provide an algorithm for automatically constructing an MSC representation for finite state asynchronous message passing protocols.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
R. Alur, K. Etessami, and M. Yannakakis. Inference of message sequence charts. In Proc. of the 22nd Int. Conf. on Software Engineering, pp. 304–313, ACM, 2000.
R. Alur, G. H. Holzmann, and D. A. Peled. An analyzer for message sequence charts. Software Concepts and Tools, 17(2):70–77, 1996.
R. Alur and M. Yannakakis. Model checking of message sequence charts. In Proc. Of CONCUR’99, LNCS no. 1664, 1999.
T. H. Cormen, C. E. Leiserson, and R. L. Rivest. Introduction to algorithms. MIT Press, Cambridge, Massachusetts, 1999.
P. Godefroid and P. Wolper. A partial approach to model checking. Information and Computation, 110(2):305–326, 1994.
E. Gunter and D. Peled. Path exploration tool. In Proc. of Tools and Algorithms for the Construction and Analysis of Systems (TACAS’99), Amsterdam, The Netherlands, LNCS 1579, pages 405–419, 1999. Springer.
L. Hélouët and P. Le Maigat. Decomposition of Message Sequence Charts. In Proc. of the 2nd Workshop on SDL and MSC (SAM2000), pp. 46–60, 2000.
J. G. Henriksen, M. Mukund, K. Narayan Kumar, and P. Thiagarajan. On message sequence graphs and finitely generated regular MSC languages. In Proc. Of ICALP’00, 2000, LNCS no. 1853, pp. 675–686, 2000.
ITU-T Recommendation Z. 120, Message Sequence Chart (MSC), 1996.
S. Mauw and M. Reniers. High-level message sequence charts. In SDL’97: Time for Testing-SDL, MSC and Trends. Proc. of the SDL Forum’97, pp. 291–306, 1997.
A. Muscholl and D. Peled. Message sequence graphs and decision problems on Mazurkiewicz traces. In Proc. MFCS’99, LNCS no. 1672, pp. 81–91, 1999.
A. Muscholl, D. Peled, and Z. Su. Deciding properties of message sequence charts. In Proc. of FoSSaCS’98, LNCS no. 1378, pp. 226–242, 1998.
A. Muscholl and D. Peled. High-level message sequence charts and finite-state communication protocols. Submitted.
D. Peled. All from One, One for All: on Model Checking Using Representatives. In Proc. of CAV’ 93, LNCS no. 697, pp. 409–423, 1993.
A. Tanenbaum, Computer Networks, Prentice Hall, 1988.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gunter, E.L., Muscholl, A., Peled, D.A. (2001). Compositional Message Sequence Charts. In: Margaria, T., Yi, W. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2001. Lecture Notes in Computer Science, vol 2031. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45319-9_34
Download citation
DOI: https://doi.org/10.1007/3-540-45319-9_34
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41865-8
Online ISBN: 978-3-540-45319-2
eBook Packages: Springer Book Archive