A Denotational Model for Interrupt-Driven Programs

被引：1

作者：

Huang, Yanhong ^{[1
]}

Zhao, Yongxin ^{[2
]}

Shi, Jianqi ^{[2
]}

Zhu, Huibiao ^{[1
]}

机构：

[1] East China Normal Univ, Shanghai Key Lab Trustworthy Comp, Shanghai 200062, Peoples R China

[2] Natl Univ Singapore, Sch Comp, Singapore, Singapore

来源：

IEEE SIXTH INTERNATIONAL CONFERENCE ON SOFTWARE TESTING, VERIFICATION AND VALIDATION WORKSHOPS (ICSTW 2013) | 2013年

基金：

新加坡国家研究基金会; 国家高技术研究发展计划(863计划); 中国国家自然科学基金;

关键词：

time; interrupt; denotational semantics;

D O I：

10.1109/ICSTW.2013.9

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

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.

引用

页码：15 / 20

页数：6