@inproceedings{d545bd5244ce408f8fb81114b277e8ec,
title = "Formal model of interrupt program from a probabilistic perspective",
abstract = "Interrupt behaviors are extremely difficult to verify and reason about in the development of operating system due to their randomicity and nondeterminism. This paper proposes a formal model of interrupt program which is an extension of Dijkstra's language of guarded commands. The probabilistic operational semantics exhibiting how the effect of interrupt is produced is explored for the interrupt program. A number of algebraic laws for the computation properties that underlie the language are established in terms of the suggested probabilistic operational semantics. Furthermore, the time constraint of the interrupt program is elaborately specified and the corresponding verification can be carried out in our framework.",
keywords = "Interrupt, Operational semantics, Probability, Verification",
author = "Yongxin Zhao and Yanhong Huang and Jifeng He and Si Liu",
year = "2011",
doi = "10.1109/ICECCS.2011.16",
language = "英语",
isbn = "9780769543819",
series = "Proceedings - 2011 16th IEEE International Conference on Engineering of Complex Computer Systems, ICECCS 2011",
pages = "87--94",
booktitle = "Proceedings - 2011 16th IEEE International Conference on Engineering of Complex Computer Systems, ICECCS 2011",
note = "16th IEEE International Conference on Engineering of Complex Computer Systems, ICECCS 2011 ; Conference date: 27-04-2011 Through 29-04-2011",
}