Investigating time properties of interrupt-driven programs

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

5 Scopus citations

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
Subtitle of host publicationFoundations and Applications - 15th Brazilian Symposium, SBMF 2012, Proceedings
Pages131-146
Number of pages16
DOIs
StatePublished - 2012
Event15th Brazilian Symposium on Formal Methods, SBMF 2012, Colocated with Third Brazilian Conference on Software:Theory and Practice, CBSoft 2012 - Natal, Brazil
Duration: 23 Sep 201228 Sep 2012

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7498 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference15th Brazilian Symposium on Formal Methods, SBMF 2012, Colocated with Third Brazilian Conference on Software:Theory and Practice, CBSoft 2012
Country/TerritoryBrazil
CityNatal
Period23/09/1228/09/12

Keywords

  • interrupt
  • operational semantics
  • time

Fingerprint

Dive into the research topics of 'Investigating time properties of interrupt-driven programs'. Together they form a unique fingerprint.

Cite this