Message Sequence Charts

  • Blaise Genest
  • Anca Muscholl
  • Doron Peled
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3098)


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.


Current Node 28th International Colloquium Message Sequence Chart Live Sequence Chart True Concurrency 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    ITU-TS recommendation Z.120 (1996)Google Scholar
  2. 2.
    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)Google Scholar
  3. 3.
    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)CrossRefGoogle Scholar
  4. 4.
    Alur, R., Holzmann, G.H., Peled, D.A.: An analyzer for message sequence charts. Software Concepts and Tools 17(2), 70–77 (1996)Google Scholar
  5. 5.
    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)Google Scholar
  6. 6.
    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)CrossRefGoogle Scholar
  7. 7.
    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)CrossRefGoogle Scholar
  8. 8.
    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)zbMATHGoogle Scholar
  9. 9.
    Brand, D., Zafiropulo, P.: On communicating finite-state machines. Journal of the ACM 30(2), 323–342 (1983)zbMATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)Google Scholar
  11. 11.
    Diekert, V., Rozenberg, G. (eds.): The Book of Traces. World Scientific, Singapore (1995)Google Scholar
  12. 12.
    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)CrossRefGoogle Scholar
  13. 13.
    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)CrossRefGoogle Scholar
  14. 14.
    Genest, B., Muscholl, A.: The structure of local choice in High-Level Message Sequence Charts (HMSC) Internal report LIAFA (2003), Available at
  15. 15.
    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)CrossRefGoogle Scholar
  16. 16.
    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 TransferCrossRefGoogle Scholar
  17. 17.
    Harel, D., Marelly, R.: Come, Let’s Play: Scenario-Based Programming Using LSCs and the Play-Engine. Springer, Heidelberg (2003)Google Scholar
  18. 18.
    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)Google Scholar
  19. 19.
    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)Google Scholar
  20. 20.
    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)CrossRefGoogle Scholar
  21. 21.
    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)CrossRefGoogle Scholar
  22. 22.
    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)CrossRefGoogle Scholar
  23. 23.
    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)CrossRefGoogle Scholar
  24. 24.
    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)CrossRefGoogle Scholar
  25. 25.
    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)CrossRefGoogle Scholar
  26. 26.
    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)CrossRefGoogle Scholar
  27. 27.
    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)CrossRefGoogle Scholar
  28. 28.
    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)CrossRefGoogle Scholar
  29. 29.
    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)Google Scholar
  30. 30.
    Sengupta, B., Cleaveland, R.: Triggered Message Sequence Charts. In: Proceedings of SIGSOFT 2002/FSE-10, pp. 167–176. ACM Press, New York (2002)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Blaise Genest
    • 1
  • Anca Muscholl
    • 1
  • Doron Peled
    • 2
  1. 1.LIAFAUniversité Paris VII & CNRSParis cedex 05France
  2. 2.Department of Computer ScienceUniversity of WarwickCoventryUnited Kingdom

Personalised recommendations