TY - GEN
T1 - A denotational model for instantaneous signal calculus
AU - Zhao, Yongxin
AU - Zhu, Longfei
AU - Zhu, Huibiao
AU - He, Jifeng
PY - 2012
Y1 - 2012
N2 - 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.
AB - 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.
UR - https://www.scopus.com/pages/publications/84868234366
U2 - 10.1007/978-3-642-33826-7_9
DO - 10.1007/978-3-642-33826-7_9
M3 - 会议稿件
AN - SCOPUS:84868234366
SN - 9783642338250
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 126
EP - 140
BT - Software Engineering and Formal Methods - 10th International Conference, SEFM 2012, Proceedings
T2 - 10th International Conference on Software Engineering and Formal Methods, SEFM 2012
Y2 - 1 October 2012 through 5 October 2012
ER -