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

    Abstract

    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
    Volume7498
    ISBN (Electronic)9783642332968
    ISBN (Print)9783642332951
    DOIs
    Publication statusPublished - 2012
    EventFormal Methods: Foundations and Applications - 15th Brazilian Symposium - Natal, Brazil
    Duration: 23 Sep 201228 Sep 2012
    Conference number: 15

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Berlin
    Volume7498

    Conference

    ConferenceFormal Methods: Foundations and Applications - 15th Brazilian Symposium
    Abbreviated titleSBMF 2012
    CountryBrazil
    CityNatal
    Period23/09/1228/09/12

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

  • Cite this

    Huang, Y., Zhao, Y., Shi, J., Zhu, H., & Qin, S. (2012). Investigating Time Properties of Interrupt-Driven Programs. In R. Gheyi , & D. Naumann (Eds.), Formal Methods: Foundations and Applications. SBMF 2012 (Vol. 7498). (Lecture Notes in Computer Science; Vol. 7498). Springer Berlin. https://doi.org/10.1007/978-3-642-33296-8_11