Semantic theories of programs with nested interrupts  

作　　者：Yanhong HUANG Jifeng HE Huibiao ZHU Yongxin ZHAO Jianqi SHI Shengchao QIN 

机构地区：[1]National Trusted Embedded Software Engineering Technology Research Center, East China Normal University, Shanghai 200062, China [2]Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai 200062, China [3]School of Computer Science and Software Engineering, Shenzhen University, Shenzhen 518060, China

出　　处：《Frontiers of Computer Science》2015年第3期331-345,共15页中国计算机科学前沿（英文版）

摘　　要：In the design of dependable software for embed- ded and real-time operating systems, time analysis is a cru- cial but extremely difficult issue, the challenge of which is exacerbated due to the randomness and nondeterminism of interrupt handling behaviors. Thus research into a theory that integrates interrupt behaviors and time analysis seems to be important and challenging. In this paper, we present a pro- gramming language to describe programs with interrupts that is comprised of two essential parts： main program and inter- rupt handling programs. We also explore a timed operational semantics and a denotational semantics to specify the mean- ings of our language. Furthermore, a strategy of deriving de- notational semantics from the timed operational semantics is provided to demonstrate the soundness of our operational se- mantics by showing the consistency between the derived de- notational semantics and the original denotational semantics.In the design of dependable software for embed- ded and real-time operating systems, time analysis is a cru- cial but extremely difficult issue, the challenge of which is exacerbated due to the randomness and nondeterminism of interrupt handling behaviors. Thus research into a theory that integrates interrupt behaviors and time analysis seems to be important and challenging. In this paper, we present a pro- gramming language to describe programs with interrupts that is comprised of two essential parts： main program and inter- rupt handling programs. We also explore a timed operational semantics and a denotational semantics to specify the mean- ings of our language. Furthermore, a strategy of deriving de- notational semantics from the timed operational semantics is provided to demonstrate the soundness of our operational se- mantics by showing the consistency between the derived de- notational semantics and the original denotational semantics.

关 键 词：embedded and real-time operating systems in-terrupts operational semantics denotational semantics semantics linking 

分 类 号：TP316.81[自动化与计算机技术—计算机软件与理论] TP312[自动化与计算机技术—计算机科学与技术]