首页|Semantic theories of programs with nested interrupts

Semantic theories of programs with nested interrupts

扫码查看
原文链接
  • NETL
  • NSTL
  • 万方数据
  • 维普
In the design of dependable software for embedded and real-time operating systems,time analysis is a crucial 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 beimportant and challenging.In this paper,we present a programming language to describe programs with interrupts that is comprised of two essential parts:main program and interrupt handling programs.We also explore a timed operational semantics and a denotational semantics to specify the meanings of our language.Furthermore,a strategy of deriving denotational semantics from the timed operational semantics is provided to demonstrate the soundness of our operational semantics by showing the consistency between the derived denotational semantics and the original denotational semantics.

embedded and real-time operating systemsinterruptsoperational semanticsdenotational semanticssemantics linking

Yanhong HUANG、Jifeng HE、Huibiao ZHU、Yongxin ZHAO、Jianqi SHI、Shengchao QIN

展开 >

National Trusted Embedded Software Engineering Technology Research Center,East China Normal University, Shanghai 200062, China

Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai 200062, China

School of Computer Science and Software Engineering, Shenzhen University, Shenzhen 518060, China

National Trusted Embedded Software Engineering Technology Research CenterNational Natural Science Foundation of ChinaNational Natural Science Foundation of ChinaNational Natural Science Foundation of ChinaNational Natural Science Foundation of ChinaNational Natural Science Foundation of ChinaNational High Technology Research and Development Program of ChinaShanghai Knowledge Service Platform ProjectShanghai Minhang Talent Project

2012FU125X15GrNos.613611360026132106461402176613730332012AA011205ZF1213

2015

10.1007/s11704-015-3251-x

计算机科学前沿
高等教育出版社

计算机科学前沿

CSTPCDCSCDSCIEI
影响因子：0.303
ISSN：2095-2228
年,卷(期)：2015.9(3)
  • 1
  • 31