Investigating Time Properties of Interrupt-Driven Programs

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

doi:10.1007/978-3-642-33296-8_11

Investigating Time Properties of Interrupt-Driven Programs

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

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 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	https://doi.org/10.1007/978-3-642-33296-8_11
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

Access to Document

10.1007/978-3-642-33296-8_11

Cite this

@inproceedings{d5f2c51ec1a74f91841cbe74df65eef8,

title = "Investigating Time Properties of Interrupt-Driven Programs",

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.",

author = "Yanhong Huang and Yongxin Zhao and Jianqi Shi and Huibiao Zhu and Shengchao Qin",

year = "2012",

doi = "10.1007/978-3-642-33296-8_11",

language = "English",

isbn = "9783642332951",

volume = "7498",

series = "Lecture Notes in Computer Science",

publisher = "Springer Berlin",

editor = "{ Gheyi }, R. and {Naumann }, D.",

booktitle = "Formal Methods: Foundations and Applications. SBMF 2012",

address = "Germany",

note = "Formal Methods: Foundations and Applications - 15th Brazilian Symposium, SBMF 2012 ; Conference date: 23-09-2012 Through 28-09-2012",

}

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, Formal Methods: Foundations and Applications - 15th Brazilian Symposium, Natal, Brazil, 23/09/12. https://doi.org/10.1007/978-3-642-33296-8_11

TY - GEN

T1 - Investigating Time Properties of Interrupt-Driven Programs

AU - Huang, Yanhong

AU - Zhao, Yongxin

AU - Shi, Jianqi

AU - Zhu, Huibiao

AU - Qin, Shengchao

N1 - Conference code: 15

PY - 2012

Y1 - 2012

N2 - 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.

AB - 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.

UR - http://dx.doi.org/10.1007/978-3-642-33296-8_11

U2 - 10.1007/978-3-642-33296-8_11

DO - 10.1007/978-3-642-33296-8_11

M3 - Conference contribution

SN - 9783642332951

VL - 7498

T3 - Lecture Notes in Computer Science

BT - Formal Methods: Foundations and Applications. SBMF 2012

A2 - Gheyi , R.

A2 - Naumann , D.

PB - Springer Berlin

T2 - Formal Methods: Foundations and Applications - 15th Brazilian Symposium

Y2 - 23 September 2012 through 28 September 2012

ER -

Investigating Time Properties of Interrupt-Driven Programs

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this