Investigating Time Properties of Interrupt-Driven Programs

Yanhong Huang, Yongxin Zhao, Jianqi Shi, Huibiao Zhu, Shengchao Qin

    Research output: Chapter in Book/Report/Conference proceedingConference contribution


    In design of dependable software for real-time embedded systems, time analysis is an important but challenging problem due in part to the randomicity and nondeterminism of interrupt handling behaviors. Time properties are generally determined by the behavior of the main program and the interrupt handling programs. In this paper, we present a small but expressive language for interrupt-driven programs and propose a timed operational semantics for it which can be used to explore various time properties. A number of algebraic laws for the computation properties that underlie the language are established on top of the proposed operational semantics. We depict a number of important time properties and illustrate them using the operational semantics via a small case study.
    Original languageEnglish
    Title of host publicationFormal Methods: Foundations and Applications. SBMF 2012
    EditorsR. Gheyi , D. Naumann
    PublisherSpringer Berlin
    ISBN (Electronic)9783642332968
    ISBN (Print)9783642332951
    Publication statusPublished - 2012
    EventFormal Methods: Foundations and Applications - 15th Brazilian Symposium - Natal, Brazil
    Duration: 23 Sept 201228 Sept 2012
    Conference number: 15

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Berlin


    ConferenceFormal Methods: Foundations and Applications - 15th Brazilian Symposium
    Abbreviated titleSBMF 2012


    Dive into the research topics of 'Investigating Time Properties of Interrupt-Driven Programs'. Together they form a unique fingerprint.

    Cite this