Skip to main content
SpringerLink
Log in

Deciding Properties of Message Sequence Charts

  • Conference paper
Scenarios: Models, Transformations and Tools

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 3466))

Abstract

Message Sequence Charts (MSCs) is a notation used in practice by protocol designers and system engineers. It is defined within an international standard (ITU Z120), and is also included, in a slightly different form, in the popular UML standard (called there sequence diagrams). We present some of the main results related to this notation, in the context of specification and automatic verification of communication protocols. We look at issues related to specification and verification. In particular, we look at automatic verification (model checking) of MSCs. We study the expressiveness of MSCs, in particular the ability to express communication protocols, and appropriate formalisms for specifying properties of MSC systems.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

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 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Alur, R., Etessami, K., Yannakakis, M.: Inference of message sequence charts. In: Proc. of the 22nd Int. Conf. on Software Engineering, pp. 304–313. ACM Press, New York (2000)

    Google Scholar 

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

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

  4. Alur, R., Peled, D., Penczek, W.: Model Checking of Causality Properties. In: Proc. of Logic in Computer Science (LICS 1995), pp. 90–100 (1995)

    Google Scholar 

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

  6. Ben-Abdulla, H., Leue, S.: Symbolic Detection of Process Divergence and Non-local Choice in Message Sequence Charts. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol. 1217, pp. 259–274. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  7. Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)

    Google Scholar 

  8. Esparza, J., Hansel, D., Rossmanith, P., Schwoon, S.: Efficient algorithms for model checking pushdown systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 232–247. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

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

  10. Genest, B.: Compositional Message Sequence Charts (CMSCs) are better to Implement than MSCs. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 429–444. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  11. 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. International Journal on Software Tools for Technology Transfer (STTT) 5(1), 78–89 (2003)

    Google Scholar 

  12. Genest, B., Muscholl, A., Peled, D.: Message sequence charts. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets. LNCS, vol. 3098, pp. 537–558. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

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

  14. Holzmann, G.: Design and Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs (1992)

    Google Scholar 

  15. ITU-T Recommendation Z.120, Message Sequence Chart, MSC (1996)

    Google Scholar 

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

  17. Henriksen, J.G., Mukund, M., Narayan Kumar, K., Thiagarajan, P.S.: 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 

  18. Henriksen, J.G., Mukund, M., Narayan Kumar, K., Thiagarajan, P.S.: 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 

  19. Kurshan, R.P.: Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, Princeton (1994)

    Google Scholar 

  20. Kuske, D.: Regular sets of infinite message sequence charts. Information and Computation (187), 80–109 (2003)

    Article  MathSciNet  Google Scholar 

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

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

  23. Mazurkiewicz, A.: Basic notions of trace theory. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency. LNCS, vol. 354, pp. 285–363. Springer, Heidelberg (1989)

    Chapter  Google Scholar 

  24. Mukund, M., Narayan Kumar, K., Sohoni, M.: Synthesizing distributed finite-state systems from MSCs. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 521–535. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  25. Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, Heidelberg (1991)

    MATH  Google Scholar 

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

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

  28. Ochmanski, E.: Recognizable trace languages. In: Diekert, V., Rozenberg, G. (eds.) The Book of Traces, pp. 167–204. World Scientific, Singapore (1995)

    Chapter  Google Scholar 

  29. Peled, D.: Specification and verification of message sequence charts. In: FORTE/PSTV 2000, pp. 139–154. Kluwer, Pisa (2000)

    Google Scholar 

  30. Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proc. of Logic in Computer Science (LICS 1986), pp. 332–344 (1986)

    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

    Anca Muscholl

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

    Doron Peled

Authors
  1. Anca Muscholl
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Doron Peled
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer and Information Science, University of Konstanz, D-78457, Konstanz, Germany

    Stefan Leue

  2. Department of Software Systems, Tampere University of Technology,  

    Tarja Johanna Systä

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Muscholl, A., Peled, D. (2005). Deciding Properties of Message Sequence Charts. In: Leue, S., Systä, T.J. (eds) Scenarios: Models, Transformations and Tools. Lecture Notes in Computer Science, vol 3466. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11495628_3

Download citation

  • DOI: https://doi.org/10.1007/11495628_3

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-26189-6

  • Online ISBN: 978-3-540-32032-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation