Semantic theories of programs with nested interrupts

Yanhong Huang, Jifeng He, Yongxin Zhao, Shengchao Qin, Jianqi Shi

    Research output: Contribution to journalArticlepeer-review


    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 be important 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.
    Original languageEnglish
    JournalFrontiers of Computer Science
    Publication statusPublished - 2015


    Dive into the research topics of 'Semantic theories of programs with nested interrupts'. Together they form a unique fingerprint.

    Cite this