Communicating Transaction Processes: An MSC-Based Model of Computation for Reactive Embedded Systems

  • Abhik Roychoudhury
  • Pazhamaneri Subramaniam Thiagarajan
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3098)


Message Sequence Charts (MSC) have been traditionally used to depict execution scenarios in the early stages of design cycle. MSCs portray inter-object interactions. Synthesizing intra-object executable specifications from an MSC-based description is a non-trivial task. Here we present a model of computation called Communicating Transaction Processes (CTP) based on MSCs from which an executable specification can be extracted in a straightforward manner. Our model describes a network of communicating processes in which the processes interact via common action labels. Each action is a non-atomic interaction described as a guarded choice of MSCs. Thus our model achieves a separation of concerns: the high-level network of processes depicting intra-process computations and control flow, while the common non-atomic communication actions capture inter-process interaction viaMSCs. We show how to extract an ordinary Petri net from a CTP model thereby leading to a standard operational semantics. We also discuss the connection of our formalism to Live Sequence Charts, an extension of MSCs which also has an executable semantics.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 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, p. 797. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  2. 2.
    ARM Limited. AMBA On-chip Bus Specification (1999)Google Scholar
  3. 3.
    Balarin, F., Lavagno, L., Passerone, C., Sangiovanni-Vincentelli, A., Watanabe, Y., Yang, G.: Concurrent execution semantics and sequential simulation algorithms for the Metropolis Meta-Model. In: International symposium on Hardware/software codesign (CODES) (2002)Google Scholar
  4. 4.
    Cadence Berkeley Laboratories, California, USA. The SMV Model Checker (1999),
  5. 5.
    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, p. 125. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  6. 6.
    Clarke, E.M., Grumberg, O., Pele, D.A.: Model Checking. MIT Press, Cambridge (1999)Google Scholar
  7. 7.
    Codesign, Simulation and Synthesis (COSY) project. Generic Interface Modules for PI-Bus (2001)Google Scholar
  8. 8.
    Damm, W., Harel, D.: LSCs: Breathing life into message sequence charts. Formal Methods in System Design 19(1) (2001)Google Scholar
  9. 9.
    Desel, J., Esparza, J.: Free Choice Petri Nets. Cambridge University Press, Cambridge (1995)zbMATHCrossRefGoogle Scholar
  10. 10.
    Douglass, B.P.: Doing Hard Time: Developing Real-time Systems using UML, Objects, Frameworks and Patterns. Addison-Wesley, Reading (1999)Google Scholar
  11. 11.
    Gajski, D.D., Zhu, J., Dmer, R., Gerstlauer, A., Zhao, S.: SpecC: Specification Language and Methodology. Kluwer Academic Publishers, Dordrecht (2000)Google Scholar
  12. 12.
    Grotker, T., Liao, S., Martin, G., Swan, S.: System Design with SystemC. Kluwer Academic Publishers, Dordrecht (2002)Google Scholar
  13. 13.
    Harel, D., Kugler, H.: From play-in scenarios to code: An achievable dream. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol. 1783, p. 22. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  14. 14.
    Harel, D., Kugler, H.: Synthesizing state-based object systems from LSC specifications. International Journal on Foundations of Computer Science 13(1) (2002)Google Scholar
  15. 15.
    Harel, D., Kugler, H., Marelly, R., Pnueli, A.: Smart play-out of behavioral requirements. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  16. 16.
    Harel, D., Marelly, R.: Come, Let’s Play: Scenario-Based Programming Using LSCs and the Play-Engine. Springer, Heidelberg (2003)Google Scholar
  17. 17.
    Hendriksen, J.G., Mukund, M., Kumar, K.N., Thiagarajan, P.S.: Message sequence graphs and finitely generated regular MSC languages. In: Welzl, E., Montanari, U., Rolim, J.D.P. (eds.) ICALP 2000. LNCS, vol. 1853, p. 675. Springer, Heidelberg (2000)Google Scholar
  18. 18.
    Holzmann, G.J.: The model checker SPIN. IEEE Transactions on Software Engineering 23(5), 279–295 (1997)CrossRefMathSciNetGoogle Scholar
  19. 19.
    Jensen, K.: Coloured Petri Nets, Basic Concepts, Analysis Methods and Practical Use. Springer, Heidelberg (1997)zbMATHGoogle Scholar
  20. 20.
    Krueger, I., Grosu, R., Scholz, P., Broy, M.: From MSCs to statecharts. In: International Workshop on Distributed and Parallel Embedded Systesms (DIPES) (1998)Google Scholar
  21. 21.
    Nielsen, M., Plotkin, G., Winskel, G.: Petri nets, event structures and domains. Theoretical Computer Science (TCS) 13 (1981)Google Scholar
  22. 22.
    Roychoudhury, A., Thiagarajan, P.S.: Communicating transaction processes. In: IEEE International Conference on Applications of Concurrency in System Design (ACSD) (2003)Google Scholar
  23. 23.
    Roychoudhury, A., Thiagarajan, P.S.: An executable specification language based on message sequence charts. In: Aichernig, B.K., Maibaum, T. (eds.) Formal Methods at the Crossroads. From Panacea to Foundational Support. LNCS, vol. 2757, pp. 226–241. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  24. 24.
    Sgroi, M., Lavagno, L.: Synthesis of embedded software using free-choice Petri nets. In: ACM Design Automation Conference (DAC) (1999)Google Scholar
  25. 25.
    Thiagarajan, P.S., et al.: Communicating Transaction Processes (CTP) project (2003),
  26. 26.
    Z. 120. Message Sequence Charts (MSC 1996) (1996)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Abhik Roychoudhury
    • 1
  • Pazhamaneri Subramaniam Thiagarajan
    • 1
  1. 1.School of ComputingNational University of SingaporeSingapore

Personalised recommendations