Abstract
The use of message sequence charts (MSCs) is popular in designing and documenting communication protocols. A recent surge of interest in MSCs has led to various algorithms for their automatic analysis, e.g., finding race conditions. In this paper we adopt a causality based temporal logic to specify properties of MSCs. This alleviates some problems that arise when specifying properties of MSCs using the traditional interleaving-based linear temporal logic: systems of MSCs are not necessarily finite state systems, leading to undecidability of LTL model checking. Even when dealing with finite state MSC systems, the set of linearizations can easily generate an exponential state space explosion. We provide an efficient model checking algorithm for systems of MSCs. Our construction models the FIFO MSC systems using a restricted version of w-automata with two successor relations. We implemented a model checking environment for MSCs as an extension to the SPIN model checking system.
The original version of this chapter was revised: The copyright line was incorrect. This has been corrected. The Erratum to this chapter is available at DOI: 10.1007/978-0-387-35533-7_26
Chapter PDF
Similar content being viewed by others
References
Alur R., Peled D., and W. Penczek (1995), Model-Checking of Causality Properties, LICS’95, 10th Symposium on Logic in Computer Science, IEEE, 1995, 90–100
Alur R., and Yannakakis M. (1999), Model Checking of Message Sequence Charts, CONCUR’99, Concurrency Theory, LNCS 1664, Eindhoven, Holland, 1999.
Alur R., Holzmann G.J., and Peled D. (1996), An Analyzer for Message Sequence Charts, Software Concepts and Tools, Vol. 17, No. 2, pp. 70–77, 1996.
Alur R. McMillan K., and Peled D. (1998), Deciding global partial-order properties, ICALP’98, Aalborg, Denmark, July, 1998, LNCS 1443, Springer, 41–52.
Clarke E.M., and Emerson E.A. (1981), Design and synthesis of synchronization skeletons using branching time temporal logic. Workshop on Logic of Programs, Yorktown Heights, NY, 1981, LNCS 131, Springer-Verlag.
Giammarresi D., Restivo A., Seibert S., and Thomas W. (1993), Monadic second-order logic over rectangular pictures and recognizability by tiling systems, Information and Computation 125 (1996), 32–45.
ITU (1993), ITU-T Recommendation Z.120, Message Sequence Chart ( MSC ), March 1993.
Holzmann G.J. (1992), Design and Validation of Computer Protocols,Prentice Hall Software Series, 1992.
Muscholl A., and Peled D. (1999), Message Sequence Graphs and Decision Problems on Mazurkiewicz Traces, Mathematical Foundations of Computer Science, Szklarska Poreba, Poland, September 1999, LNCS 1672, Springer, 81–91.
Muscholl A., Peled D., and Su Z. (1998), Deciding Properties for Message Sequence Charts, FoSSaCS 1998, Foundations of Software Science and Computation Structures, Lisbon, Portugal, LNCS 1378, 226–242.
Vardi M.Y., Wolper P. (1986), An automata-theoretic approach to automatic program verification. Proc. 1st Annual Symposium on Logic in Computer Science IEEE, 1986, 332–344.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 IFIP International Federation for Information Processing
About this chapter
Cite this chapter
Peled, D. (2000). Specification and Verification of Message Sequence Charts. In: Bolognesi, T., Latella, D. (eds) Formal Methods for Distributed System Development. PSTV FORTE 2000 2000. IFIP — The International Federation for Information Processing, vol 55. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35533-7_9
Download citation
DOI: https://doi.org/10.1007/978-0-387-35533-7_9
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4757-5264-9
Online ISBN: 978-0-387-35533-7
eBook Packages: Springer Book Archive