Abstract
In this paper we explore an observation-oriented denotational semantics for instantaneous signal calculus which contains all conceptually instantaneous reactions of signal calculus for event-based synchronous languages. The healthiness conditions are studied for especially dealing with the emission of signals. Every instantaneous reaction can be identified as denoting a healthiness function over the set of events which describe the state of the system and its environment. The normal form, surprisingly, has the comparatively elegant and straightforward denotational semantic definition. Furthermore, a set of algebraic laws concerning the distinct features for instantaneous signal calculus is investigated. All algebraic laws can be established in the framework of our semantic model, i.e., if the equality of two differently written instantaneous reactions is algebraically provable, the two reactions are also equivalent with respect to the denotational semantics.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Berry, G.: The foundations of esterel. In: Proof, Language, and Interaction, Essays in Honour of Robin Milner, pp. 425–454. The MIT Press (2000)
Berry, G., Gonthier, G.: The esterel synchronous programming language: Design, semantics, implementation. Science Computer Program 19(2), 87–152 (1992)
Goguen, J.A., Thatcher, J.W., Wagner, E.G., Wright, J.B.: Initial algebra semantics and continuous algebras. Jounrnal of the ACM 24(1), 68–95 (1977)
Hoare, C.A.R., Hayes, I.J., He, J., Morgan, C., Roscoe, A.W., Sanders, J.W., Sørensen, I.H., Spivey, J.M., Sufrin, B.: Laws of programming. Commun. ACM 30(8), 672–686 (1987)
Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice Hall International Series in Computer Science (1998)
Hoare, C.A.R., He, J., Sampaio, A.: Normal form approach to compiler design. Acta Inf. 30(8), 701–739 (1993)
Laplante, P.A.: Real-Time Systems Design and Analysis: An Engineer’s Handbook, 2nd edn. IEEE Press (1997)
Lee, E.A.: Cyber-Physical Systems - are computing foundations adequate? Technical report, Department of EECS, UC Berkeley (2006)
Maddux, R.D.: Relation-algebraic semantics. Theoretical Computer Science 160(1&2), 1–85 (1996)
Mousavi, M.R.: Causality in the semantics of esterel: Revisited. In: SOS: Structural Operational Semantics. EPTCS, vol. 18, pp. 32–45 (2009)
Nissanke, N.: Real time systems. Prentice Hall series in computer science. Prentice Hall (1997)
Roscoe, A.W., Hoare, C.A.R.: The laws of occam programming. Theoretical Computer Science 60, 177–229 (1988)
Scott, D., Strachey, C.: Towards a mathematical semantics for computer languages. Technical Report PRG-6,Oxford Univeristiy Computer Laboratory (1971)
Tardieu, O., de Simone, R.: Loops in esterel. ACM Transaction in Embedded Computer Systems 4(4), 708–750 (2005)
Tarski, A.: A lattice-theoretical fixpoint theorem and its application. Pacific Journal of Mathmatics 5(2), 285–309 (1955)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zhao, Y., Zhu, L., Zhu, H., He, J. (2012). A Denotational Model for Instantaneous Signal Calculus. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds) Software Engineering and Formal Methods. SEFM 2012. Lecture Notes in Computer Science, vol 7504. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33826-7_9
Download citation
DOI: https://doi.org/10.1007/978-3-642-33826-7_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-33825-0
Online ISBN: 978-3-642-33826-7
eBook Packages: Computer ScienceComputer Science (R0)