Semantic theories of programs with nested interrupts

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

References

[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

[3] Hills T. Structured interrupts. ACM SIGOPS Operating Systems Review, 1993, 27: 51-68

[4] Regehra J, Cooprider N. Interrupt verification via thread verification. Electronic Notes in Theoretical Computer Science, 2007, 174(9): 139-150

[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

[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

[7] Kleiman S, Eykholt J. Interrupts as threads. ACM SIGOPS Operating Systems Review, 1995, 29: 21-26

[8] Brylow D, Damgaard N, Palsberg J. Static checking of interrupt-driven software. In: Proceedings of International Conference on Software Engineering. 2001, 47-56

[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

[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

[11] Brylow D, Palsberg J. Deadline analysis of interrupt-driven software. IEEE Transactions on Software Engineering, 2004, 30: 634-655

[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

[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

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

[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

[22] Brookes S. Full abstraction for a shared-variable parallel language. Information and Computation, 1996, 127: 145-163

[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

[27] Hartog J, Vink E. Verifying probabilistic programs using a Hoare like logic. International Journal of Foundations of Computer Science, 2002, 13: 315-340

[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

[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

RIGHTS & PERMISSIONS

Higher Education Press and Springer-Verlag Berlin Heidelberg