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 language | English |
---|---|
Title of host publication | Formal Methods: Foundations and Applications. SBMF 2012 |
Editors | R. Gheyi , D. Naumann |
Publisher | Springer Berlin |
Volume | 7498 |
ISBN (Electronic) | 9783642332968 |
ISBN (Print) | 9783642332951 |
DOIs | |
Publication status | Published - 2012 |
Event | Formal Methods: Foundations and Applications - 15th Brazilian Symposium - Natal, Brazil Duration: 23 Sept 2012 → 28 Sept 2012 Conference number: 15 |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer Berlin |
Volume | 7498 |
Conference
Conference | Formal Methods: Foundations and Applications - 15th Brazilian Symposium |
---|---|
Abbreviated title | SBMF 2012 |
Country/Territory | Brazil |
City | Natal |
Period | 23/09/12 → 28/09/12 |