Skip to main content

Netcharts: Bridging the Gap between HMSCs and Executable Specifications

  • Conference paper
CONCUR 2003 - Concurrency Theory (CONCUR 2003)

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

Included in the following conference series:

Abstract

We define a new notation called netcharts for describing sets of message sequence chart scenarios (MSCs). Netcharts correspond to a distributed version of High-level Message Sequence Charts (HMSCs). Netcharts improve on HMSCs in two respects.

  • Netcharts admit a natural and direct translation into communicating finite-state machines, unlike HMSCs, for which the realization problem is nontrivial.

  • Netcharts can describe all regular MSC languages (sets of MSCs in which channel capacities have a finite upper bound), unlike HMSCs, which can only describe finitely-generated regular MSC languages.

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

Access this chapter

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

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

  3. Booch, G., Jacobson, I., Rumbaugh, J.: Unified Modeling Language User Guide. Addison-Wesley, Reading (1997)

    Google Scholar 

  4. Caillaud, B., Darondeau, P., Helouet, L., Lesventes, G.: HMSCs as partial specifications.. with PNs as completions. In: Cassez, F., Jard, C., Rozoy, B., Dermot, M. (eds.) MOVEP 2000. LNCS, vol. 2067, pp. 125–152. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  5. Desel, J., Esparza, J.: Free Choice Petri Nets. In: Cambridge Tracts in Theoretical Computer Science 40. Cambridge University Press, Cambridge (1995)

    Google Scholar 

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

    Chapter  Google Scholar 

  7. Harel, D., Gery, E.: Executable object modelling with statecharts. IEEE Computer, 31–42 (July 1997)

    Google Scholar 

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

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

  10. ITU-TS Recommendation Z.120: Message Sequence Chart (MSC). ITU-TS, Geneva (1997)

    Google Scholar 

  11. Mauw, S., Reniers, M.A.: High-level message sequence charts. In: Proc. 8th SDL Forum, SDL 1997: Time for Testing — SDL, MSC and Trends, pp. 291–306. Elsevier, Amsterdam (1997)

    Google Scholar 

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

    Chapter  Google Scholar 

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

  14. Roychoudhury, A., Thiagarajan, P.S.: Communicating transaction processes. In: Proc. ACSD 2003. IEEE Press, Los Alamitos (2003) (to appear)

    Google Scholar 

  15. Rudolph, E., Graubmann, P., Grabowski, J.: Tutorial on message sequence charts. Computer Networks and ISDN Systems — SDL and MSC 28 (1996)

    Google Scholar 

  16. Sgroi, M., Kondratyev, A., Watanabe, Y., Sangiovanni-Vincentelli, A.: Synthesis of Petri nets from MSC-based specifications (unpublished manuscript)

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Mukund, M., Kumar, K.N., Thiagarajan, P.S. (2003). Netcharts: Bridging the Gap between HMSCs and Executable Specifications. In: Amadio, R., Lugiez, D. (eds) CONCUR 2003 - Concurrency Theory. CONCUR 2003. Lecture Notes in Computer Science, vol 2761. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45187-7_20

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-45187-7_20

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-40753-9

  • Online ISBN: 978-3-540-45187-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics