Probabilistic Denotational Semantics for an Interrupt Modelling Language

Yanhong Huang; Yongxin Zhao; Shengchao Qin; Jifeng He

doi:10.1109/ICECCS.2015.35

Probabilistic Denotational Semantics for an Interrupt Modelling Language

Yanhong Huang, Yongxin Zhao, Shengchao Qin, Jifeng He

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English
Title of host publication	20th International Conference on Engineering of Complex Computer Systems, ICECCS 2015, Gold Coast, Australia, December 9-12, 2015
Publisher	IEEE
ISBN (Electronic)	978-1-4673-8581-7
DOIs	https://doi.org/10.1109/ICECCS.2015.35
Publication status	Published - 18 Jan 2016
Event	20th International Conference on Engineering of Complex Computer Systems (ICECCS) - Queensland , Gold Coast, Australia Duration: 9 Dec 2015 → 12 Dec 2015 Conference number: 20

Publication series

Name	Engineering of Complex Computer Systems, IEEE International Conference on

Conference

Conference	20th International Conference on Engineering of Complex Computer Systems (ICECCS)
Country/Territory	Australia
City	Gold Coast
Period	9/12/15 → 12/12/15

Access to Document

10.1109/ICECCS.2015.35

Cite this

Huang, Y., Zhao, Y., Qin, S., & He, J. (2016). Probabilistic Denotational Semantics for an Interrupt Modelling Language. In 20th International Conference on Engineering of Complex Computer Systems, ICECCS 2015, Gold Coast, Australia, December 9-12, 2015 (Engineering of Complex Computer Systems, IEEE International Conference on). IEEE. https://doi.org/10.1109/ICECCS.2015.35

@inproceedings{33890d0b6b64490eab2bc92efaef6f0e,

title = "Probabilistic Denotational Semantics for an Interrupt Modelling Language",

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

author = "Yanhong Huang and Yongxin Zhao and Shengchao Qin and Jifeng He",

year = "2016",

month = jan,

day = "18",

doi = "10.1109/ICECCS.2015.35",

language = "English",

series = "Engineering of Complex Computer Systems, IEEE International Conference on",

publisher = "IEEE",

booktitle = "20th International Conference on Engineering of Complex Computer Systems, ICECCS 2015, Gold Coast, Australia, December 9-12, 2015",

note = "20th International Conference on Engineering of Complex Computer Systems (ICECCS) ; Conference date: 09-12-2015 Through 12-12-2015",

}

Huang, Y, Zhao, Y, Qin, S & He, J 2016, Probabilistic Denotational Semantics for an Interrupt Modelling Language. in 20th International Conference on Engineering of Complex Computer Systems, ICECCS 2015, Gold Coast, Australia, December 9-12, 2015. Engineering of Complex Computer Systems, IEEE International Conference on, IEEE, 20th International Conference on Engineering of Complex Computer Systems (ICECCS), Gold Coast, Australia, 9/12/15. https://doi.org/10.1109/ICECCS.2015.35

Probabilistic Denotational Semantics for an Interrupt Modelling Language. / Huang, Yanhong; Zhao, Yongxin; Qin, Shengchao et al.
20th International Conference on Engineering of Complex Computer Systems, ICECCS 2015, Gold Coast, Australia, December 9-12, 2015. IEEE, 2016. (Engineering of Complex Computer Systems, IEEE International Conference on).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Probabilistic Denotational Semantics for an Interrupt Modelling Language

AU - Huang, Yanhong

AU - Zhao, Yongxin

AU - Qin, Shengchao

AU - He, Jifeng

N1 - Conference code: 20

PY - 2016/1/18

Y1 - 2016/1/18

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

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

U2 - 10.1109/ICECCS.2015.35

DO - 10.1109/ICECCS.2015.35

M3 - Conference contribution

T3 - Engineering of Complex Computer Systems, IEEE International Conference on

BT - 20th International Conference on Engineering of Complex Computer Systems, ICECCS 2015, Gold Coast, Australia, December 9-12, 2015

PB - IEEE

T2 - 20th International Conference on Engineering of Complex Computer Systems (ICECCS)

Y2 - 9 December 2015 through 12 December 2015

ER -

Probabilistic Denotational Semantics for an Interrupt Modelling Language

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this