Skip to main content
SpringerLink
Log in
Book cover

Advanced Course on Petri Nets

ACPN 2003: Lectures on Concurrency and Petri Nets pp 537–558Cite as

Message Sequence Charts

  • Chapter

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 3098))

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.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. ITU-TS recommendation Z.120 (1996)

    Google Scholar 

  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. 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)

    Chapter  Google Scholar 

  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. 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. 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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    MATH  Google Scholar 

  9. Brand, D., Zafiropulo, P.: On communicating finite-state machines. Journal of the ACM 30(2), 323–342 (1983)

    Article  MATH  MathSciNet  Google Scholar 

  10. Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)

    Google Scholar 

  11. Diekert, V., Rozenberg, G. (eds.): The Book of Traces. World Scientific, Singapore (1995)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  14. 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

  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)

    Chapter  Google Scholar 

  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 Transfer

    Chapter  Google Scholar 

  17. Harel, D., Marelly, R.: Come, Let’s Play: Scenario-Based Programming Using LSCs and the Play-Engine. Springer, Heidelberg (2003)

    Google Scholar 

  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. 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. 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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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. Sengupta, B., Cleaveland, R.: Triggered Message Sequence Charts. In: Proceedings of SIGSOFT 2002/FSE-10, pp. 167–176. ACM Press, New York (2002)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LIAFA, Université Paris VII & CNRS, 2, pl. Jussieu, case 7014, 75251, Paris cedex 05, France

    Blaise Genest & Anca Muscholl

  2. Department of Computer Science, University of Warwick, Coventry, CV4 7AL, United Kingdom

    Doron Peled

Authors
  1. Blaise Genest
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Anca Muscholl
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Doron Peled
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Applied Computer Science, Catholic University of Eichstätt-Ingolstadt,  

    Jörg Desel

  2. Institut für Informatik, Humboldt-Universität zu Berlin, Unter den Linden 6, 10099, Berlin, Germany

    Wolfgang Reisig

  3. , Leiden Center of Advanced Computer Science (LIACS), Leiden University, Niels Bohrweg 1, 2333, Leiden, CA, The Netherlands

    Grzegorz Rozenberg

Rights and permissions

Reprints 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

Publish with us

Policies and ethics

Search

Navigation