A Denotational Model for Interrupt-Driven Programs

作者：Huang, Yanhong^*; Zhao, Yongxin; Shi, Jianqi; Zhu, Huibiao

来源：6th IEEE International Conference on Software Testing, Verification and Validation (ICST), Luxembourg, 2013-03-18 To 2013-03-22.

DOI：10.1109/ICSTW.2013.9

• time
• interrupt
• denotational semantics

In design of dependable software for real-time embedded systems, the interrupt mechanism plays an important role. Due to the randomicity and nondeterminism of interrupt handling behaviors, the analysis about program behaviors as well as time properties is an important but challenging problem. In a previous work, we presented a small but expressive language for interrupt-driven programs, and suggested a timed operational semantics to specify the meaning of the programs. In this paper, we explore a denotational semantics under a discrete time model for the interrupt-driven programming language. It can deal with the features of the language. We also define a transition which can link the operational semantics and denotational semantics.

• 出版日期2013
• 单位华东师范大学