Abstract
Message sequence charts (MSC) are a graphical notation standardized by the ITU and used for the description of communication scenarios between asynchronous processes. This survey compares MSCs and communicating finite-state automata, presenting two fundamental validation problems on MSCs, model-checking and implementability.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
ITU-TS recommendation Z.120 (1996)
Alur, R., Etessami, K., Yannakakis, M.: Inference of Message Sequence Charts. In: Proceedings of the 22nd International Conference on Software Engineering, Limerick, Ireland, pp. 304–313. ACM, New York (2000)
Alur, R., Etessami, K., Yannakakis, M.: Realizability and verification of MSC graphs. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, pp. 797–808. Springer, Heidelberg (2001)
Alur, R., Holzmann, G.H., Peled, D.A.: An analyzer for message sequence charts. Software Concepts and Tools 17(2), 70–77 (1996)
Alur, R., Peled, D., Penczek, W.: Model-checking of causality properties. In: Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science (LICS 1995). IEEE, Los Alamitos (1995)
Alur, R., Yannakakis, M.: Model checking of message sequence charts. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 114–129. Springer, Heidelberg (1999)
Ben-Abdallah, H., Leue, S.: Syntactic detection of process divergence and nonlocal choice in message sequence charts. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol. 1217, pp. 259–274. Springer, Heidelberg (1997)
Berard, B., Bidoit, M., Finkel, A., Laroussinie, F., Petit, A., Petrucci, L., Schnoebelen, P.: Systems and Software Verification, Model-Checking Techniques and Tools. Springer, Heidelberg (2001)
Brand, D., Zafiropulo, P.: On communicating finite-state machines. Journal of the ACM 30(2), 323–342 (1983)
Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)
Diekert, V., Rozenberg, G. (eds.): The Book of Traces. World Scientific, Singapore (1995)
Genest, B., Minea, M., Muscholl, A., Peled, D.: Specifying and verifying partial order properties using template MSCs. In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol. 2987, pp. 195–210. Springer, Heidelberg (2004)
Genest, B., Muscholl, A.: Pattern matching and membership for Hierarchical Message Sequence Charts. In: Rajsbaum, S. (ed.) LATIN 2002. LNCS, vol. 2286, pp. 326–340. Springer, Heidelberg (2002)
Genest, B., Muscholl, A.: The structure of local choice in High-Level Message Sequence Charts (HMSC) Internal report LIAFA (2003), Available at http://www.crans.org/~genest/report_lc.ps
Genest, B., Muscholl, A., Seidl, H., Zeitoun, M.: Infinite-state High-level MSCs: Model-checking and realizability. In: Widmayer, P., Triguero, F., Morales, R., Hennessy, M., Eidenbenz, S., Conejo, R. (eds.) ICALP 2002. LNCS, vol. 2380, pp. 657–668. Springer, Heidelberg (2002)
Gunter, E., Muscholl, A., Peled, D.: Compositional Message Sequence Charts. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 496–511. Springer, Heidelberg (2001); Journal version to appear in the International Journal on Software Tools for Technology Transfer
Harel, D., Marelly, R.: Come, Let’s Play: Scenario-Based Programming Using LSCs and the Play-Engine. Springer, Heidelberg (2003)
Hélouët, L., Jard, C.: Conditions for synthesis of communicating automata from HMSCs. In: 5th International Workshop on Formal Methods for Industrial Critical Systems, Berlin (2000)
Hélouët, L., Le Maigat, P.: Decomposition of Message Sequence Charts. In: Proceedings of the 2nd Workshop on SDL and MSC (SAM 2000), Col de Porte, Grenoble, pp. 46–60 (2000)
Henriksen, J.G., Mukund, M., Narayan Kumar, K., Thiagarajan, P.: On Message Sequence Graphs and finitely generated regular MSC languages. In: Welzl, E., Montanari, U., Rolim, J.D.P. (eds.) ICALP 2000. LNCS, vol. 1853, pp. 675–686. Springer, Heidelberg (2000)
Henriksen, J.G., Mukund, M., Narayan Kumar, K., Thiagarajan, P.: Regular collections of Message Sequence Charts. In: Nielsen, M., Rovan, B. (eds.) MFCS 2000. LNCS, vol. 1893, pp. 405–414. Springer, Heidelberg (2000)
Kuske, D.: A Further Step towards a Theory of Regular MSC Languages. In: Alt, H., Ferreira, A. (eds.) STACS 2002. LNCS, vol. 2285, pp. 489–500. Springer, Heidelberg (2002)
Lohrey, M.: Safe realizability of High-level Message Sequence Charts. In: Brim, L., Jančar, P., Křetínský, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 177–192. Springer, Heidelberg (2002)
Madhusudan, P.: Reasoning about sequential and branching behaviours of Message Sequence Graphs. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, pp. 809–820. Springer, Heidelberg (2001)
Mukund, M., Narayan Kumar, K., Thiagarajan, P.S.: Netcharts: bridging the gap between HMSCs and executable specifications. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 296–310. Springer, Heidelberg (2003)
Morin, R.: Recognizable Sets of Message Sequence Charts. In: Alt, H., Ferreira, A. (eds.) STACS 2002. LNCS, vol. 2285, pp. 523–540. Springer, Heidelberg (2002)
Muscholl, A., Peled, D.: Message sequence graphs and decision problems on Mazurkiewicz traces. In: Kutyłowski, M., Wierzbicki, T., Pacholski, L. (eds.) MFCS 1999. LNCS, vol. 1672, pp. 81–91. Springer, Heidelberg (1999)
Muscholl, A., Peled, D., Su, Z.: Deciding properties of Message Sequence Charts. In: Nivat, M. (ed.) FOSSACS 1998. LNCS, vol. 1378, pp. 226–242. Springer, Heidelberg (1998)
Peled, D.: Specification and verification of Message Sequence Charts. In: Proceedings of Formal Techniques for Distributed System Development, FORTE/PSTV 2000, Pisa, Italy, pp. 139–154 (2000)
Sengupta, B., Cleaveland, R.: Triggered Message Sequence Charts. In: Proceedings of SIGSOFT 2002/FSE-10, pp. 167–176. ACM Press, New York (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Genest, B., Muscholl, A., Peled, D. (2004). Message Sequence Charts. In: Desel, J., Reisig, W., Rozenberg, G. (eds) Lectures on Concurrency and Petri Nets. ACPN 2003. Lecture Notes in Computer Science, vol 3098. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-27755-2_15
Download citation
DOI: https://doi.org/10.1007/978-3-540-27755-2_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22261-3
Online ISBN: 978-3-540-27755-2
eBook Packages: Springer Book Archive