A denotational model for interrupt-driven programs

Yanhong Huang; Yongxin Zhao; Jianqi Shi; Huibiao Zhu

doi:10.1109/ICSTW.2013.9

A denotational model for interrupt-driven programs

Yanhong Huang, Yongxin Zhao, Jianqi Shi, Huibiao Zhu

Software Engineering Institute

National University of Singapore

Research output: Contribution to conference › Paper › peer-review

2 Scopus citations

Abstract

In design of dependable software for real-time embedded systems, the interrupt mechanism plays an important role. Due to the random city and no determinism of interrupt handling behaviors, the analysis about program behaviors as well as time properties is an important but challenging problem. In a previous work, we presented a small but expressive language for interrupt-driven programs, and suggested a timed operational semantics to specify the meaning of the programs. In this paper, we explore a denotational semantics under a discrete time model for the interrupt-driven programming language. It can deal with the features of the language. We also define a transition which can link the operational semantics and denotational semantics.

Original language	English
Pages	15-20
Number of pages	6
DOIs	https://doi.org/10.1109/ICSTW.2013.9
State	Published - 2013
Event	IEEE 6th International Conference on Software Testing, Verification and Validation Workshops, ICSTW 2013 - Luxembourg, Luxembourg Duration: 18 Mar 2013 → 20 Mar 2013

Conference

Conference	IEEE 6th International Conference on Software Testing, Verification and Validation Workshops, ICSTW 2013
Country/Territory	Luxembourg
City	Luxembourg
Period	18/03/13 → 20/03/13

Keywords

denotational semantics
interrupt
time

Access to Document

10.1109/ICSTW.2013.9

Cite this

@conference{43e51561cf7741d3aadff90a7336539b,

title = "A denotational model for interrupt-driven programs",

abstract = "In design of dependable software for real-time embedded systems, the interrupt mechanism plays an important role. Due to the random city and no determinism of interrupt handling behaviors, the analysis about program behaviors as well as time properties is an important but challenging problem. In a previous work, we presented a small but expressive language for interrupt-driven programs, and suggested a timed operational semantics to specify the meaning of the programs. In this paper, we explore a denotational semantics under a discrete time model for the interrupt-driven programming language. It can deal with the features of the language. We also define a transition which can link the operational semantics and denotational semantics.",

keywords = "denotational semantics, interrupt, time",

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

year = "2013",

doi = "10.1109/ICSTW.2013.9",

language = "英语",

pages = "15--20",

note = "IEEE 6th International Conference on Software Testing, Verification and Validation Workshops, ICSTW 2013 ; Conference date: 18-03-2013 Through 20-03-2013",

}

TY - CONF

T1 - A denotational model for interrupt-driven programs

AU - Huang, Yanhong

AU - Zhao, Yongxin

AU - Shi, Jianqi

AU - Zhu, Huibiao

PY - 2013

Y1 - 2013

N2 - In design of dependable software for real-time embedded systems, the interrupt mechanism plays an important role. Due to the random city and no determinism of interrupt handling behaviors, the analysis about program behaviors as well as time properties is an important but challenging problem. In a previous work, we presented a small but expressive language for interrupt-driven programs, and suggested a timed operational semantics to specify the meaning of the programs. In this paper, we explore a denotational semantics under a discrete time model for the interrupt-driven programming language. It can deal with the features of the language. We also define a transition which can link the operational semantics and denotational semantics.

AB - In design of dependable software for real-time embedded systems, the interrupt mechanism plays an important role. Due to the random city and no determinism of interrupt handling behaviors, the analysis about program behaviors as well as time properties is an important but challenging problem. In a previous work, we presented a small but expressive language for interrupt-driven programs, and suggested a timed operational semantics to specify the meaning of the programs. In this paper, we explore a denotational semantics under a discrete time model for the interrupt-driven programming language. It can deal with the features of the language. We also define a transition which can link the operational semantics and denotational semantics.

KW - denotational semantics

KW - interrupt

KW - time

UR - https://www.scopus.com/pages/publications/84883408956

U2 - 10.1109/ICSTW.2013.9

DO - 10.1109/ICSTW.2013.9

M3 - 论文

AN - SCOPUS:84883408956

SP - 15

EP - 20

T2 - IEEE 6th International Conference on Software Testing, Verification and Validation Workshops, ICSTW 2013

Y2 - 18 March 2013 through 20 March 2013

ER -

A denotational model for interrupt-driven programs

Abstract

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this