Skip to main content
SpringerLink
Log in

Unifying Operational Semantics with Algebraic Semantics for Instantaneous Reactions

  • Conference paper
Unifying Theories of Programming (UTP 2012)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 7681))

Included in the following conference series:

  • 447 Accesses

Abstract

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.

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

    Chapter  Google Scholar 

  2. Berry, G., Gonthier, G.: The Esterel synchronous programming language: Design, semantics, implementation. Science of Computer Programming (SCP) 19(2), 87–152 (1992)

    Article  MATH  Google Scholar 

  3. Berry, G.: The Constructive Semantics of Pure Esterel, Draft version (1999), ftp://ftp-sop.inria.fr/meije/esterel/papers/constructiveness3.ps.gz

  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. Potop-Butucaru, D., Edwards, S.A., Berry, G.: Compiling Esterel, pp. I–XXI, 1–335. Springer (2007)

    Google Scholar 

  6. Shyamasundar, R.K., Ramesh, S.: Real Time Programming: Languages, Specification and Verifcations. World Scientific Publishing (2009)

    Google Scholar 

  7. Mousavi, M.: Causality in the Semantics of Esterel: Revisited. Electronic Proceedings in Theoretical Computer Science 18, 32–45 (2010)

    Article  Google Scholar 

  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)

    Chapter  Google Scholar 

  9. Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  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. 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. Boussinot, F.: Reactive C: An extension of C to program reactive systems. Software Practice Experience 21(4), 401–428 (1991)

    Article  Google Scholar 

  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. Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages and Compution. Addison-Wesley (1979)

    Google Scholar 

  15. Nicollin, X., Sifakis, J.: The algebra of timed processes, ATP: Theory and application. Inf. Comput. 114(1), 131–178 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  17. Reed, G.M., Roscoe, A.W.: The timed failures-stablity model for CSP. Theor. Comput. Sci. 211(1-2), 85–127 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  18. Yovine, S.: Kronos: A verification tool for real-time systems. STTT 1(1-2), 123–133 (1997)

    Article  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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 

Download references

Author information

Authors and Affiliations

  1. Shanghai Key Laboratory of Trustworthy Computing Software Engineering Institute, East China Normal University, China

    Chengcheng Wu & Huibiao Zhu

  2. School of Computing, National University of Singapore, Singapore

    Yongxin Zhao

Authors
  1. Chengcheng Wu
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Yongxin Zhao
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Huibiao Zhu
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Laboratoire de Recherche en Informatique (LRI), Université Paris-Sud, Gif-sur-Yvette, France

    Burkhart Wolff , Marie-Claude Gaudel  & Abderrahmane Feliachi ,  & 

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Wu, C., Zhao, Y., Zhu, H. (2013). Unifying Operational Semantics with Algebraic Semantics for Instantaneous Reactions. In: Wolff, B., Gaudel, MC., Feliachi, A. (eds) Unifying Theories of Programming. UTP 2012. Lecture Notes in Computer Science, vol 7681. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-35705-3_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-35705-3_9

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-35704-6

  • Online ISBN: 978-3-642-35705-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation