Deadline analysis of interrupt-driven software

ABSTRACT

Real-time, reactive, and embedded systems are widely 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 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 multi-resolution 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.

REFERENCES

• 1: Rajeev Alur , David L. Dill, A theory of timed automata, Theoretical Computer Science, v.126 n.2, p.183-235, April 25, 1994 [doi>10.1016/0304-3975(94)90010-8 ]
• 2: Rajeev Alur , Thomas A. Henzinger, Logics and Models of Real Time: A Survey, Proceedings of the Real-Time: Theory in Practice, REX Workshop, p.74-106, June 03-07, 1991
• 3: G. Bernat, A. Burns, and A. Wellings. Portable WCET analysis using Java byte code. In Proc. ERTS 2000, pp.81--88, Jun 2000.
• 4: Dennis W. Brylow , Jens Palsberg, Static checking of interrupt-driven software, 2003
• 5: Dennis Brylow , Niels Damgaard , Jens Palsberg, Static checking of interrupt-driven software, Proceedings of the 23rd International Conference on Software Engineering, p.47-56, May 12-19, 2001, Toronto, Ontario, Canada
• 6: L. Cardelli. Type systems. In The Computer Science and Engineering Handbook, chapter 103, pp.2208--2236. CRC Press, Boca Raton, FL, 1997.
• 7: E. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, Cambridge, MA, Jan 2000.
• 8: Matteo Corti , Roberto Brega , Thomas Gross, Approximation of Worst-Case Execution Time for Preemptive Multitasking Systems, Proceedings of the ACM SIGPLAN Workshop on Languages, Compilers, and Tools for Embedded Systems, p.178-198, June 18, 2000
• 9: J. Engblom and A. Ermedahl. Modeling complex flows for WCET analysis. In Proc. RTSS 2000, Nov 2000.
• 10: Jakob Engblom , Bengt Jonsson, Processor Pipelines and Their Properties for Static WCET Analysis, Proceedings of the Second International Conference on Embedded Software, p.334-348, October 07-09, 2002
• 11: S. Z. Guyer and C. Lin. Client-driven pointer analysis. In Proc. SAS 03, pp.214--236, 2003.
• 12: Mary Jean Harrold , James A. Jones , Tongyu Li , Donglin Liang , Alessandro Orso , Maikel Pennings , Saurabh Sinha , S. Alexander Spoon , Ashish Gujarathi, Regression test selection for Java software, Proceedings of the 16th ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, p.312-326, October 14-18, 2001, Tampa Bay, FL, USA
• 13: Tim Lindholm , Frank Yellin, Java Virtual Machine Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
• 14: Steven S. Muchnick, Advanced compiler design and implementation, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1998
• 15: Stefan M. Petters , Georg Färber, Making Worst Case Execution Time Analysis for Hard Real-Time Tasks on State of the Art Processors Feasible, Proceedings of the Sixth International Conference on Real-Time Computing Systems and Applications, p.442, December 13-15, 1999
• 16: John Plevyak , Andrew A. Chien, Precise concrete type inference for object-oriented languages, Proceedings of the ninth annual conference on Object-oriented programming systems, language, and applications, p.324-340, October 23-28, 1994, Portland, Oregon, United States
• 17: Debra J. Richardson , Stephanie Leif Aha , T. Owen O'Malley, Specification-based test oracles for reactive systems, Proceedings of the 14th international conference on Software engineering, p.105-118, May 11-15, 1992, Melbourne, Australia [doi>10.1145/143062.143100]
• 18: Olin Grigsby Shivers, Control-flow analysis of higher-order languages of taming lambda, Carnegie Mellon University, Pittsburgh, PA, 1991
• 19: Henrik Theiling , Christian Ferdinand , Reinhard Wilhelm, Fast and Precise WCET Prediction by Separated Cache andPath Analyses, Real-Time Systems, v.18 n.2-3, p.157-179, May 2000
• 20: K. W. Tindell , A. Burns , A. J. Wellings, An extendible approach for analyzing fixed priority hard real-time tasks, Real-Time Systems, v.6 n.2, p.133-151, March 1994 [doi>10.1007/BF01088593]
• 21: Emilio Vivancos , Christopher Healy , Frank Mueller , David Whalley, Parametric Timing Analysis, Proceedings of the ACM SIGPLAN workshop on Languages, compilers and tools for embedded systems, p.88-93, August 2001, Snow Bird, Utah, United States
• 22: Zhichen Xu , Barton P. Miller , Thomas Reps, Safety checking of machine code, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.70-82, June 18-21, 2000, Vancouver, British Columbia, Canada

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

General Terms:
Algorithms, Measurement, Reliability

Keywords:
multi-resolution static analysis, real time, testing oracles