Abstract
Message sequence charts (MSCs) are used in the design phase of a distributed system to record intended system behaviors. They serve as informal documentation of design requirements that are referred to throughout the design process and even in the final system integration and acceptance testing. We show that message sequence charts are open to a variety of semantic interpretations. The meaning of an MSC can depend on, for instance, whether one allows or denies the possibility of message loss or message overtaking, and on the particulars of the message queuing policy to be adopted.
We describe an analysis tool that can perform automatic checks on message sequence charts and can alert the user to the existence of subtle design errors, for any predefined or user-specified semantic interpretation of the chart. The tool can also be used to specify time constraints on message delays, and can then return useful additional timing information, such as the minimum and the maximum possible delays between pairs of events.
Chapter PDF
Similar content being viewed by others
References
R. Alur, A. Itai, R.P. Kurshan, M. Yannakakis. Timing verification by successive approximation. Information and Computation 118(1), pp. 142–157, 1995.
D.L. Dill. Timing assumptions and verification of finite-state concurrent systems. In Automatic Verification Methods for Finite State Systems, LNCS 407, pp. 197–212, 1989.
R.W. Floyd. Algorithm 97 (Shortest Path). Communications of the ACM 5 (1962), pp. 365.
G.J. Holzmann. Design and Validation of Computer Protocols, Prentice Hall Software Series, 1991.
ITU-T Recommendation Z.120, Message Sequence Chart (MSC), March 1993. (Includes [7] as Annex B.)
P.B. Ladkin, S. Leue. What do message sequence charts mean. In Formal Description Techniques, VI 1994 (FORTE'94), Elsevier, pp. 301–315.
S. Mauw, M.A. Reniers. An algebraic semantics of basic message sequence charts. The Computer Journal, 37(4) (1994).
J. Ousterhout. Tcl and the Tk toolkit, Addison-Wesley, 1994.
C.H. Papadimitriou, K. Steiglitz. Combinatorial Optimization-Algorithms and Complexity, Prentice-Hall, 1982.
T.H. Cormen, C.E. Leiserson, R.L. Rivest, Introduction to Algorithms, MIT press, 1990.
S. Warshall. A theorem on boolean matrices. Journal of the ACM, 9 (1962), pp. 11–12.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Alur, R., Holzmann, G.J., Peled, D. (1996). An analyzer for message sequence charts. In: Margaria, T., Steffen, B. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 1996. Lecture Notes in Computer Science, vol 1055. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61042-1_37
Download citation
DOI: https://doi.org/10.1007/3-540-61042-1_37
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61042-7
Online ISBN: 978-3-540-49874-2
eBook Packages: Springer Book Archive