Unifying Operational Semantics with Algebraic Semantics for Instantaneous Reactions

  • Chengcheng Wu
  • Yongxin Zhao
  • Huibiao Zhu
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7681)


The signal calculus for event-based synchronous languages is developed for the specification and programming of embedded systems. This paper first explores a structural operational semantics for conceptually instantaneous reactions of the signal calculus, which exhibits how the effectiveness of such reactions is produced. Further, we investigate the unifying theory of operational semantics and algebraic semantics for instantaneous reactions. On one hand, all the algebraic laws characterizing the primitives and the combinators can be established in terms of the suggested structural operational semantics which claims the soundness of the algebraic semantics. On the other hand, reactions which are equivalent from the operational perspective can be reduced to the same normal form and this demonstrates the relative completeness of algebraic semantics with respect to the operational semantics.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Zhao, Y., Jifeng, H.: Towards a Signal Calculus for Event-Based Synchronous Languages. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 1–13. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  2. 2.
    Berry, G., Gonthier, G.: The Esterel synchronous programming language: Design, semantics, implementation. Science of Computer Programming (SCP) 19(2), 87–152 (1992)zbMATHCrossRefGoogle Scholar
  3. 3.
    Berry, G.: The Constructive Semantics of Pure Esterel, Draft version (1999),
  4. 4.
    Tini, S.: Structural Operational Semantics for Synchronous Languages. PhD thesis, Dipartimento di Informaticá, Universita degli Studi di Pisa, Pisa, Italy (2000)Google Scholar
  5. 5.
    Potop-Butucaru, D., Edwards, S.A., Berry, G.: Compiling Esterel, pp. I–XXI, 1–335. Springer (2007)Google Scholar
  6. 6.
    Shyamasundar, R.K., Ramesh, S.: Real Time Programming: Languages, Specification and Verifcations. World Scientific Publishing (2009)Google Scholar
  7. 7.
    Mousavi, M.: Causality in the Semantics of Esterel: Revisited. Electronic Proceedings in Theoretical Computer Science 18, 32–45 (2010)CrossRefGoogle Scholar
  8. 8.
    Alur, R., Dill, D.L.: Automata for Modeling Real-time Systems. In: Paterson, M. (ed.) ICALP 1990. LNCS, vol. 443, pp. 322–335. Springer, Heidelberg (1990)CrossRefGoogle Scholar
  9. 9.
    Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)MathSciNetzbMATHCrossRefGoogle Scholar
  10. 10.
    Behrmann, G., David, A., Larson, K.G.: A tutorial on UPPAAL. In: International School on Formal Methods for the Design of Computer, Communication, and Software Systems (2004)Google Scholar
  11. 11.
    Berry, G.: The foundations of Esterel. In: Proof, Language, and Interaction, Essays in Honour of Robin Milner, pp. 425–454. The MIT Press (2000)Google Scholar
  12. 12.
    Boussinot, F.: Reactive C: An extension of C to program reactive systems. Software Practice Experience 21(4), 401–428 (1991)CrossRefGoogle Scholar
  13. 13.
    He, J.: From CSP to hybrid systems. In: Roscure, A.W. (ed.) A Classical Mind, Essays in Honour of C.A.R. Hoare, pp. 171–189. Prentice-Hall International (1994)Google Scholar
  14. 14.
    Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages and Compution. Addison-Wesley (1979)Google Scholar
  15. 15.
    Nicollin, X., Sifakis, J.: The algebra of timed processes, ATP: Theory and application. Inf. Comput. 114(1), 131–178 (1994)MathSciNetzbMATHCrossRefGoogle Scholar
  16. 16.
    Reed, G.M., Roscoe, A.W.: A Timed Model for Communicating Sequential Processes. In: Kott, L. (ed.) ICALP 1986. LNCS, vol. 226, pp. 314–323. Springer, Heidelberg (1986)CrossRefGoogle Scholar
  17. 17.
    Reed, G.M., Roscoe, A.W.: The timed failures-stablity model for CSP. Theor. Comput. Sci. 211(1-2), 85–127 (1999)MathSciNetzbMATHCrossRefGoogle Scholar
  18. 18.
    Yovine, S.: Kronos: A verification tool for real-time systems. STTT 1(1-2), 123–133 (1997)zbMATHCrossRefGoogle Scholar
  19. 19.
    Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: The Maude 2.0 System. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 76–87. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  20. 20.
    Clavel, M., Durán, F.F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: Maude Manual (Version 2.6) (January 2011)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Chengcheng Wu
    • 1
  • Yongxin Zhao
    • 2
  • Huibiao Zhu
    • 1
  1. 1.Shanghai Key Laboratory of Trustworthy Computing Software Engineering InstituteEast China Normal UniversityChina
  2. 2.School of ComputingNational University of SingaporeSingapore

Personalised recommendations