This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Deadline Analysis of Interrupt-Driven Software
October 2004 (vol. 30 no. 10)
pp. 634-655
Real-time, reactive, and embedded systems are increasingly used throughout society (e.g., flight control, railway signaling, vehicle management, medical devices, and many others). For real-time, interrupt-driven software, timely interrupt handling is part of correctness. It is vital for software verification in such systems to check that all specified deadlines for interrupt handling will be met. Such verification is a daunting task because of the large number of different possible interrupt arrival scenarios. For example, for a Z86-based microcontroller, there can be up to six interrupt sources and each interrupt can arrive during any clock cycle. Verification of such systems has traditionally relied upon lengthy and tedious testing; even under the best of circumstances, testing is likely to cover only a fraction of the state space in interrupt-driven systems. This paper presents the Zilog Architecture Resource Bounding Infrastructure (ZARBI), a tool for deadline analysis of interrupt-driven Z86-based software. The main idea is to use static analysis to significantly decrease the required testing effort by automatically identifying and isolating the segments of code that need the most testing. Our tool combines multiresolution static analysis and testing oracles in such a way that only the oracles need to be verified by testing. Each oracle specifies the worst-case execution time from one program point to another, which is then used by the static analysis to improve precision. For six commercial microcontroller systems, our experiments show that a moderate number of testing oracles are sufficient to do precise deadline analysis.

[1] Agere Systems, Inc., APP550 Student Training Guide, 1905A Kramer Lane Suite 100, Austin, Texas 78758, May 2003.
[2] A.V. Aho, R. Sethi, and J.D. Ullman, Compilers: Principles, Techniques and Tools. Addison-Wesley, 1985.
[3] M. Alt, C. Ferdinand, F. Martin, and R. Wilhelm, “Cache Behavior Prediction by Abstract Interpretation,” Proc. SAS 96: Int'l Static Analysis Symp., 1996.
[4] P. Altenbernd, “On the False Path Problem in Hard Real-Time Programs,” Proc. ERTS 96: Eighth EuroMicro Workshop Real-Time Systems, pp. 102-107, June 1996.
[5] R. Alur and D.L. Dill, “A Theory of Timed Automata,” Theoretical Computer Science, vol. 126, no. 2, pp. 183-235, 1994.
[6] R. Alur and T.A. Henzinger, “Logics and Models of Real Time: A Survey,” Real-Time: Theory in Practice, J.W. de Bakker, et al., eds., 1992.
[7] G. Balakrishnan and T. Reps, “Analyzing Memory Accesses in x86 Executables,” Proc. CC 04: 13th Int'l Conf. Compiler Construction, vol. 2985, pp. 5-23, Mar. 2004.
[8] G. Bernat, A. Burns, and A. Wellings, “Portable Worst-Case Execution Time Analysis Using Java Byte Code,” Proc. 12th Euromicro Conf. Real-Time Systems, pp. 81-88, June 2000.
[9] D. Brylow, N. Damgaard, and J. Palsberg, “Static Checking of Interrupt Driven Software,” Proc. ICSE 01: 23rd Int'l Conf. Software Eng., pp. 47-56, June 2001.
[10] D.W. Brylow, “Static Analysis of Interrupt-Driven Software,” PhD thesis, Purdue Univ., 2003.
[11] A. Burns and A. Wellings, Real-Time Systems and Programming Languages, third ed. Addison Wesley, 2001.
[12] L. Cardelli, “Type Systems,” The Computer Science and Engineering Handbook, A.B. Tucker, ed., chapter 103, pp. 2208-2236, 1997.
[13] E. Clarke, O. Grumberg, and D. Peled, Model Checking. MIT Press, Jan. 2000.
[14] M. Corti, R. Brega, and T. Gross, “Approximation of Worst-Case Execution Time for Preemptive Multitasking Systems,” Proc. LCTES 00: ACM SIGPLAN Workshop Languages, Compilers and Tools for Embedded Systems, 2000.
[15] P. Cousot and R. Cousot, “Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints,” Proc. POPL 77: Fourth Ann. ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages, pp. 238-252, 1977.
[16] M.B. Dwyer, “Data Flow Analysis for Verifying Correctness Properties of Concurrent Programs,” PhD thesis, Univ. Massachusetts, Amherst, Sept. 1995.
[17] E.A. Emerson, “Temporal and Modal Logic,” Handbook of Theoretical Computer Science (vol. B): Formal Models and Semantics, J. van Leeuwen, et al., eds., pp. 995-1072, 1990.
[18] J. Engblom and A. Ermedahl, “Modeling Complex Flows for Worst-Case Execution Time Analysis,” Proc. RTSS 00: 21st IEEE Real-Time Systems Symp., Nov. 2000.
[19] J. Engblom, A. Ermedahl, M. Sjödin, J. Gustafsson, and H. Hansson, “Worst-Case Execution-Time Analysis for Embedded Real-Time Systems,” Software Tools for Technology Transfer, vol. 14, 2000.
[20] J. Engblom and B. Jonsson, “Processor Pipelines and Their Properties for Static WCET Analysis,” Proc. EMSOFT 02: Second Int'l Conf. Embedded Software, A. Sangiovanni-Vincentelli and J. Sifakis, eds., pp. 334-348, Oct. 2002.
[21] C. Ferdinand, R. Heckmann, M. Langenbach, F. Martin, M. Schmidt, H. Theiling, S. Thesing, and R. Wilhelm, “Reliable and Precise WCET Determination for a Real-Life Processor,” Proc. EMSOFT 01: First Int'l Workshop Embedded Software, T.A. Henzinger and C.M. Kirsch, eds., Oct. 2001.
[22] C. Ferdinand, F. Martin, and R. Wilhelm, “Applying Compiler Techniques to Cache Behavior Prediction,” Proc. LCTRTS 97: ACM SIGPLAN Workshop Languages, Compilers and Tools for Real-Time Systems, pp. 37-46, 1997.
[23] D. Gay, P. Levis, J.R. vonBehren, M. Welsh, E.A. Brewer, and D.E. Culler, “The nesC Language: A Holistic Approach to Networked Embedded Systems,” Proc. PLDI 03: ACM SIGPLAN Conf. Programming Language Design and Implementation, pp. 1-11, 2003.
[24] J. Gustafsson, B. Lisper, N. Bermudo, C. Sandberg, and L. Sjöberg, “A Prototype Tool for Flow Analysis of C Programs,” Proc. WCET 02: Second IEEE Int'l Workshop Worst Case Execution Time Analysis, pp. 10-13, June 2002.
[25] S.Z. Guyer and C. Lin, “Client-Driven Pointer Analysis,” Proc. SAS 03: 10th Ann. Int'l Static Analysis Symp., R. Cousot, ed., pp. 214-236, 2003.
[26] M.J. Harrold, J.A. Jones, T. Li, D. Liang, and A. Gujarathi, “Regression Test Selection for Java Software,” Proc. OOPSLA 01: 16th Ann. ACM SIGPLAN Conf. Object-Oriented Programming Systems, Languages, and Applications, pp. 312-326, 2001.
[27] C.A. Healy, M. Sjödin, V. Rustagi, D.B. Whalley, and R. vanEngelen, “Supporting Timing Analysis by Automatic Bounding of Loop Iterations,” J. Real-Time Systems, vol. 18, nos. 2/3, pp. 129-156, 2000.
[28] C.A. Healy and D.B. Whalley, “Automatic Detection and Exploitation of Branch Constraints for Timing Analysis,” IEEE Trans. Software Eng., vol. 28, no. 8, pp. 763-781, Aug. 2002.
[29] T.A. Henzinger, R. Jhala, and R. Majumdar, “Race Checking by Context Inference,” of PLDI 04: Int'l Conf. Programming Language Design and Implementation, pp. 1-13, 2004.
[30] ILOG, “CPLEX mixed integer optimizer,” http://www.ilog.com/products/cplex/product mip.cfm, 2003.
[31] T. Lindholm and F. Yell, The Java Virtual Machine Specification, second ed. Addison-Wesley, Apr. 1999.
[32] D. McAllester, “On the Complexity Analysis of Static Analyses,” Proc. SAS 99: Int'l Static Analysis Symp., 1999.
[33] P.C. McGeer and R.K. Brayton, Integrating Functional and Temporal Domains in Logic Design. Kluwer Academic, May 1991.
[34] T. Mitra and A. Roychoudhury, “A Framework to Model Branch Prediction for WCET Analysis,” Proc. WCET 02: Second IEEE Int'l Workshop Worst Case Execution Time Analysis, pp. 68-71, June 2002.
[35] J.C. Mogul, R.F. Rashid, and M.J. Accetta, “The Packet Filter: An Efficient Mechanism for User-Level Network Code,” Proc. SOSP 87: 11th ACM Symp. Operating Systems Principles, pp. 39-51, 1987.
[36] S. Muchnick, Advanced Compiler Design and Implementation. Morgan Kaufmann, 1997.
[37] G. Naumovich, G.S. Avrunin, and L.A. Clarke, “Data Flow Analysis for Checking Properties of Concurrent Java Programs,” Proc. ICSE 99: 21st Int'l Conf. Software Eng., pp. 399-410, May 1999.
[38] G. Naumovich and L.A. Clarke, “Extending FLAVERS to Check Properties on Infinite Executions of Concurrent Software Systems,” Technical Report TR-CIS-2000-02, Polytechnic Univ., Apr. 2000.
[39] F. Nielson, H.R. Nielson, and C. Hank, Principles of Program Analysis. Springer, 1999.
[40] P. Notebaert, “lp_solve: Mixed Integer Linear Program Solver,” ftp://ftp.es.ele.tue.nl/publp_solve, 2003.
[41] J. Palsberg and M.I. Schwartzbach, “Object-Oriented Type Inference,” Proc. OOPSLA 91: Sixth Ann. ACM SIGPLAN Conf. Object-Oriented Programming Systems, Languages, and Applications, pp. 146-161, 1991.
[42] S. Petters and G. Färber, “Making Worst Case Execution Time Analysis for Hard Real-Time Tasks on State of the Art Processors Feasible,” Proc. RTCSA 99: Sixth Int'l Conf. Real-Time Computing Systems and Applications, pp. 442-449, 1999.
[43] J. Plevyak and A.A. Chien, “Precise Concrete Type Inference for Object-Oriented Languages,” Proc. OOPSLA 94: Ninth Ann. Conf. Object-Oriented Programming Systems, Language, and Applications, pp. 324-340, 1994.
[44] A. Podelski, “Model Checking as Constraint Solving,” Proc. SAS 00: Int'l Static Analysis Symp., 2000.
[45] P. Puschner and C. Koza, “Calculating the Maximum Execution Time of Real-Time Programs,” J. Real-Time Systems, vol. 1, no. 2, pp. 159-176, Sept. 1989.
[46] P.P. Puschner and A.V. Schedl, “Computing Maximum Task Execution Times— A Graph-Based Approach,” J. Real-Time Systems, vol. 13, no. 1, pp. 67-91, 1997.
[47] J. Regehr, A. Reid, and K. Webb, “Eliminating Stack Overflow by Abstract Interpretation,” Proc. EMSOFT 03: Third Int'l Conf. Embedded Software, 2003.
[48] T. Reps, “Undecidability of Context-Sensitive Data-Independence Analysis,” ACM Trans. Programming Languages and Systems (TOPLAS), vol. 22, no. 1, pp. 162-186, 2000.
[49] D.J. Richardson, S.L. Aha, and T.O. O'Malley, “Specification-Based Test Oracles for Reactive Systems,” Proc. ICSE 92: 14th Int'l Conf. Software Eng., pp. 105-118, 1992.
[50] R. Sedgewick, Algorithms in C, Part 5: Graph Algorithms. third ed., Addison-Wesley, 2001.
[51] M. Sharir and A. Pnueli, “Two Approaches to Interprocedural Data Flow Analysis,” Program Flow Analysis, Theory and Applications, S. Muchnick and N. Jones, eds., 1981.
[52] O. Shivers, “Control-Flow Analysis of Higher-Order Languages,” PhD thesis, Carnegie Mellon Univ., May 1991.
[53] H. Theiling, C. Ferdinand, and R. Wilhelm, “Fast and Precise WCET Prediction by Separated Cache and Path Analyses,” J. Real-Time Systems, vol. 18, nos. 2/3, pp. 157-179, 2000.
[54] K.W. Tindell, A. Burns, and A.J. Wellings, “An Extendible Approach for Analysing Fixed Priority Hard Real-Time Tasks,” J. Real-Time Systems, vol. 6, no. 2, pp. 133-152, Mar. 1994.
[55] F. Tip and J. Palsberg, “Scalable Propagation-Based Call Graph Construction Algorithms,” Proc. OOPSLA 00: 15th Ann. ACM SIGPLAN Conf. Object-Oriented Programming Systems, Languages, and Applications, pp. 281-293, 2000.
[56] E. Vivancos, C. Healy, F. Mueller, and D. Whalley, “Parametric Timing Analysis,” Proc. LCTES 01: ACM SIGPLAN Workshop Languages, Compilers and Tools for Embedded Systems, pp. 88-93, 2001.
[57] J. Wegener and F. Mueller, “A Comparison of Static Analysis and Evolutionary Testing for the Verification of Timing Constraints,” J. Real-Time Systems, vol. 21, no. 3, pp. 241-268, Nov. 2001.
[58] Z. Xu, B.P. Miller, and T. Reps, “Safety Checking of Machine Code,” Proc. PLDI 00: ACM SIGPLAN Conf. Programming Language Design and Implementation, 2000.
[59] Zilog, Inc., Z86E30/E31/E40 Preliminary Product Specification, Campbell, Calif., 1998, http://www.zilog.com/pdfs/z8otpe303140.pdf .

Index Terms:
Real time, multiresolution static analysis, testing oracles.
Citation:
Dennis Brylow, Jens Palsberg, "Deadline Analysis of Interrupt-Driven Software," IEEE Transactions on Software Engineering, vol. 30, no. 10, pp. 634-655, Oct. 2004, doi:10.1109/TSE.2004.64
Usage of this product signifies your acceptance of the Terms of Use.