Probabilistic Denotational Semantics for an Interrupt Modelling Language

Yanhong Huang, Yongxin Zhao, Shengchao Qin, Jifeng He

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

    Abstract

    Interrupts play an important role in real time and embedded systems. It is purposely designed to handle unexpected and emergent issues. However, the randomicity of interrupts brings some potential safety problems, i.e., too frequently interrupt handling would cause the interrupted program to miss its deadline. It is therefore difficult to precisely predict and formally reason about a program's behavior in the presence of interrupts. In this paper, we move one step forward by proposing a probabilistic denotational model for an interrupt modeling language that is capable of describing programs with nested interrupts, to characterise the formal semantics of such programs from a quantitative perspective under Hoare and He's UTP framework. On top of the denotational model, we also present a set of algebraic laws involving distinct features. Our model sets up a semantic foundation for the analysis and reasoning about programs with nested interrupts for embedded systems.
    Original languageEnglish
    Title of host publication20th International Conference on Engineering of Complex Computer Systems, ICECCS 2015, Gold Coast, Australia, December 9-12, 2015
    PublisherIEEE
    ISBN (Electronic)978-1-4673-8581-7
    DOIs
    Publication statusPublished - 18 Jan 2016
    Event20th International Conference on Engineering of Complex Computer Systems (ICECCS) - Queensland , Gold Coast, Australia
    Duration: 9 Dec 201512 Dec 2015
    Conference number: 20

    Publication series

    NameEngineering of Complex Computer Systems, IEEE International Conference on

    Conference

    Conference20th International Conference on Engineering of Complex Computer Systems (ICECCS)
    CountryAustralia
    CityGold Coast
    Period9/12/1512/12/15

    Fingerprint Dive into the research topics of 'Probabilistic Denotational Semantics for an Interrupt Modelling Language'. Together they form a unique fingerprint.

    Cite this