TY - GEN
T1 - Probabilistic Denotational Semantics for an Interrupt Modelling Language
AU - Huang, Yanhong
AU - Zhao, Yongxin
AU - Qin, Shengchao
AU - He, Jifeng
N1 - Publisher Copyright:
© 2015 IEEE.
PY - 2016/1/15
Y1 - 2016/1/15
N2 - Interrupts play an important role in real time and embedded systems. It is purposely designed to handle unexpected and emergent issues. However, the randomicity of interrupts brings some potential safety problems, i.e., too frequently interrupt handling would cause the interrupted program to miss its deadline. It is therefore difficult to precisely predict and formally reason about a program's behavior in the presence of interrupts. In this paper, we move one step forward by proposing a probabilistic denotational model for an interrupt modeling language that is capable of describing programs with nested interrupts, to characterise the formal semantics of such programs from a quantitative perspective under Hoare and He's UTP framework. On top of the denotational model, we also present a set of algebraic laws involving distinct features. Our model sets up a semantic foundation for the analysis and reasoning about programs with nested interrupts for embedded systems.
AB - Interrupts play an important role in real time and embedded systems. It is purposely designed to handle unexpected and emergent issues. However, the randomicity of interrupts brings some potential safety problems, i.e., too frequently interrupt handling would cause the interrupted program to miss its deadline. It is therefore difficult to precisely predict and formally reason about a program's behavior in the presence of interrupts. In this paper, we move one step forward by proposing a probabilistic denotational model for an interrupt modeling language that is capable of describing programs with nested interrupts, to characterise the formal semantics of such programs from a quantitative perspective under Hoare and He's UTP framework. On top of the denotational model, we also present a set of algebraic laws involving distinct features. Our model sets up a semantic foundation for the analysis and reasoning about programs with nested interrupts for embedded systems.
KW - Denotational Semantics
KW - Interrupt
KW - Probabilistic Semantics
KW - Unifying Theories of Programming
UR - https://www.scopus.com/pages/publications/84964884638
U2 - 10.1109/ICECCS.2015.35
DO - 10.1109/ICECCS.2015.35
M3 - 会议稿件
AN - SCOPUS:84964884638
T3 - Proceedings of the IEEE International Conference on Engineering of Complex Computer Systems, ICECCS
SP - 160
EP - 169
BT - Proceedings - 2015 20th International Conference on Engineering of Complex Computer Systems, ICECCS 2015
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 20th International Conference on Engineering of Complex Computer Systems, ICECCS 2015
Y2 - 9 December 2015 through 11 December 2015
ER -