Semantic theories of programs with nested interrupts

doi:10.1007/s11704-015-3251-x

Front. Comput. Sci.

2015, Vol. 9

Issue (3) : 331-345 https://doi.org/10.1007/s11704-015-3251-x

RESEARCH ARTICLE

Semantic theories of programs with nested interrupts

Yanhong HUANG^1,²(

),Jifeng HE²,Huibiao ZHU^2,^*(

),Yongxin ZHAO²,Jianqi SHI^1,²,Shengchao QIN³

1. National Trusted Embedded Software Engineering Technology Research Center, ast China Normal University, Shanghai 200062, China
2. Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai 200062, China
3. School of Computer Science and Software Engineering, Shenzhen University, Shenzhen 518060, China

Download: PDF(424 KB)
Export: BibTeX | EndNote | Reference Manager | ProCite | RefWorks

Abstract

In the design of dependable software for embedded and real-time operating systems, time analysis is a crucial but extremely difficult issue, the challenge of which is exacerbated due to the randomness and nondeterminism of interrupt handling behaviors. Thus research into a theory that integrates interrupt behaviors and time analysis seems to be important and challenging. In this paper, we present a programming language to describe programs with interrupts that is comprised of two essential parts: main program and interrupt handling programs. We also explore a timed operational semantics and a denotational semantics to specify the meanings of our language. Furthermore, a strategy of deriving denotational semantics from the timed operational semantics is provided to demonstrate the soundness of our operational semantics by showing the consistency between the derived denotational semantics and the original denotational semantics.

Keywords embedded and real-time operating systems interrupts operational semantics denotational semantics semantics linking

Corresponding Author(s): Huibiao ZHU

Issue Date: 18 May 2015

Cite this article:

Yanhong HUANG,Jifeng HE,Huibiao ZHU, et al. Semantic theories of programs with nested interrupts[J]. Front. Comput. Sci., 2015, 9(3): 331-345.

URL:

https://academic.hep.com.cn/fcs/EN/10.1007/s11704-015-3251-x
https://academic.hep.com.cn/fcs/EN/Y2015/V9/I3/331

1	Regehra J. Safe and Structured Use of Interrupts in Real-time and Embedded Software. Handbook of Real-Time and Embedded Systems, CRC Press. 2007, 1-15
2	Tarski A. A Lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 1955, 5(2): 285-309 https://doi.org/10.2140/pjm.1955.5.285
3	Hills T. Structured interrupts. ACM SIGOPS Operating Systems Review, 1993, 27: 51-68 https://doi.org/10.1145/160551.160556
4	Regehra J, Cooprider N. Interrupt verification via thread verification. Electronic Notes in Theoretical Computer Science, 2007, 174(9): 139-150 https://doi.org/10.1016/j.entcs.2007.04.002
5	Feng X, Shao Z, Guo Y, Dong Y. Certifying low-level programs with hardware interrupts and preemptive threads. Journal of Automated Reasoning, 2009, 42: 301-347 https://doi.org/10.1007/s10817-009-9118-9
6	Leslie I, McAuley D, Black R, Roscoe T, Barham P, Evers D, Fairbairns R, Hyden E. The design and implementation of an operating system to support distributed multimedia applications. IEEE Journal of Selected Areas in Communications, 1996, 14: 1280-1297 https://doi.org/10.1109/49.536480
7	Kleiman S, Eykholt J. Interrupts as threads. ACM SIGOPS Operating Systems Review, 1995, 29: 21-26 https://doi.org/10.1145/202213.202217
8	Brylow D, Damgaard N, Palsberg J. Static checking of interrupt-driven software. In: Proceedings of International Conference on Software Engineering. 2001, 47-56 https://doi.org/10.1109/icse.2001.919080
9	Palsberg J, Ma D. A typed interrupt calculus. In: Proceedings of the 7th International Symposium on Formal Techniques in Real-Time and Fault Tolerant Systems. 2002, 291-310 https://doi.org/10.1007/3-540-45739-9_18
10	Chatterjee K, Ma D, Majumdar R, Zhao T, Henzinger T A, Palsberg J. Stack size analysis for interrupt-driven programs. In: Proceedings of International Static Analysis Symposium. 2003, 109-126 https://doi.org/10.1007/3-540-44898-5_7
11	Brylow D, Palsberg J. Deadline analysis of interrupt-driven software. IEEE Transactions on Software Engineering, 2004, 30: 634-655 https://doi.org/10.1109/TSE.2004.64
12	Bérard B, Haddad S. Interrupt timed automata. In: Proceedings of the 12th International Conference on Foundations of Software Science and Computation Structures. 2009, 197-211 https://doi.org/10.1007/978-3-642-00596-1_15
13	Bérard B, Haddad S, Sassolas M. Real time properties for interrupt timed automata. In: Proceedings of the 17th International Symposium on Temporal Representation and Reasoning. 2010, 69-76 https://doi.org/10.1109/time.2010.11
14	Bérard B, Haddad S, Sassolas M. Interrupt timed automata: verification and expressiveness. In: Proceedings of Formal Methods in System Design. 2012, 41-87
15	Li G, Yuen S, Adachi M. Environmental simulation of real-time systems with nested interrupts. In: Proceedings of the 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering. 2009, 21-28 https://doi.org/10.1109/tase.2009.12
16	Baeten J C M, Bergstra J A, Klop J W. Syntax and defining equations for an interrupt mechanism in process algebra. Fundamenta Information IX(2), 1986, 9: 127-168
17	Diertens B. New Features in PSF I- Interrupts, Disrupts, and Priorities. Report P9417, Programming Research Group- University of Amsterdam. 1994, 5-17
18	Engels A, Cobben T. Interrupt and disrupt in MSC: possibilities and problems. In: Proceedings of the 1st Workshop of the SDL Forum Society on SDL and MSC. 1998, 1-4
19	Hoare C A R. Communicating Sequential Processes. Prentice Hall, 1985
20	Hoare C A R, He J. Unifying Theories of Programming. Prentice Hall, 1998
21	Hoare C A R, He J. From algebra to operational semantics. Information Process Letter, 1993, 45: 75-80 https://doi.org/10.1016/0020-0190(93)90219-Y
22	Brookes S. Full abstraction for a shared-variable parallel language. Information and Computation, 1996, 127: 145-163 https://doi.org/10.1006/inco.1996.0056
23	Bakker J, Vink E. Control flow semantics. The MIT Press, 1996
24	Hartog J. Probabilistic extensions of semantic models. Dissertation for PhD Degree, Vrije University, The Netherlands, 2002
25	Hartog J, Vink E. Mixing up nondeterminism and probability: a preliminary report. Electrontic Notes Theoretical Computer Science, 1999, 22: 88-110
26	Hartog J, Vink E, Bakker J. Metric semantics and full abstractness for action refinement and probabilistic choice. Electronic Notes in Theoretical Computer Science, 2001, 40: 72-99 https://doi.org/10.1016/S1571-0661(05)80038-6
27	Hartog J, Vink E. Verifying probabilistic programs using a Hoare like logic. International Journal of Foundations of Computer Science, 2002, 13: 315-340 https://doi.org/10.1142/S012905410200114X
28	Zhu H, Bowen J P, He J. From operational semantics to denotational semantics for Verilog. In: Proceedings of the 11th Advanced Research Working Conference on Correct Hardware Design and Verification Methods. 2001, 449-464
29	Zhu H, He J, Li J, Pu G, Bowen J P. Linking denotational semantics with operational semantics for web services. Innvoations Systems and Software Engineering, 2010, 6: 283-298 https://doi.org/10.1007/s11334-010-0134-z
30	Zhu H, Yang F, He J, Bowen J P, Sanders J W, Qin S. Linking operational semantics and algebraic semantics for a probabilistic timed shared-variable language. The Journal of Logic and Algebraic Programming, 2012, 81: 2-25 https://doi.org/10.1016/j.jlap.2011.06.003

[1]

Supplementary Material-Highlights in 3-page ppt

Download

[1]	Qin LI,Yongxin ZHAO,Huibiao ZHU,Jifeng HE. A UTP semantic model for Orc language with execution status and fault handling[J]. Front. Comput. Sci., 2014, 8(5): 709-725.
[2]	Shuling WANG, Qin SHU, Yijing LIU, Zongyan QIU, . A semantic model of confinement and Locality Theorem[J]. Front. Comput. Sci., 2010, 4(1): 28-46.

Viewed

Full text

Abstract

Cited

Shared

Discussed