ABSTRACT
Static worst-case execution time analysis of real-time tasks is based on abstract models that capture the timing behavior of the processor on which the tasks run. For complex processors, task-level execution time bounds are obtained by a state exploration which involves the abstract model and the program. Partial state space exploration is not sound. A full exploration can become too expensive. We present a novel symbolic method for WCET analysis based on abstract pipeline models which produces sound results and is scalable in terms of the considered hardware states.
- AbsInt. aiT WCET Analyzers. http://www.absint.com/ait, 2000.Google Scholar
- C. Berg. PLRU cache domino effects. In 6th Intl. Workshop on Worst-Case Execution Time (WCET) Analysis. Schloss Dagstuhl, Germany, 2006.Google Scholar
- M. Berndl, O. Lhotak, F. Qian, L. J. Hendren, and N. Umanee. Points-to analysis using BDDs. In PLDI, pages 103--114, 2003. Google ScholarDigital Library
- A. Betts, G. Bernat, R. Kirner, P. Puschner, and I. Wenzel. WCET Coverage for Pipelines. Technical report, 2006.Google Scholar
- D. Beyer, T. A. Henzinger, R. Jhala, and R. Majumdar. The software model checker Blast. STTT, 9(5-6):505--525, 2007. Google ScholarCross Ref
- R. K. Brayton, G. D. Hachtel, A. L. Sangiovanni-Vincentelli, F. Somenzi, A. Aziz, S.-T. Cheng, S. A. Edwards, S. P. Khatri, Y. Kukimoto, A. Pardo, S. Qadeer, R. K. Ranjan, S. Sarwary, T. R. Shiple, G. Swamy, and T. Villa. VIS: A System for Verification and Synthesis. In CAV, pages 428--432, 1996. Google ScholarDigital Library
- R. Bryant. Graph based algorithms for boolean function manipulation. In IEEE Transactions on Computers, 1986. Google ScholarDigital Library
- J. Burch, E. Clarke, K. McMillan, D. Dill, and J. Hwang. Symbolic model checking: 1020 states and beyond. IEEE Comp. Soc. Press, 1990.Google Scholar
- S.-T. Cheng. Compiling Verilog into Automata. Technical report, Electronics Research Lab, Univ. of California, Berkeley, CA 94720, 1994.Google Scholar
- E. M. Clarke, O. Grumberg, H. Hiraishi, S. Jha, D. E. Long, K. L. McMillan, and L. A. Ness. Verification of the Futurebus+ Cache Coherence Protocol. In CHDL, pages 15--30, 1993. Google ScholarDigital Library
- P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Los Angeles, California, 1977. Google ScholarDigital Library
- EDN. DSP Benchmarks. In EDN - Electronic Design, Strategy, News, Sept. 1988.Google Scholar
- J. Engblom. Processor Pipelines and Static Worst-Case Execution Time Analysis. PhD thesis, Uppsala University, 2002.Google Scholar
- C. Ferdinand. Cache Behavior Prediction for Real-Time Systems. PhD thesis, Saarland University, 1997.Google Scholar
- 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. In Proceedings of EMSOFT 2001, LNCS 2211, 2001. Google ScholarDigital Library
- M. Fujita, Y. Matsunaga, and T. Kakuda. On variable ordering of binary decision diagrams for the application of multi-level logic synthesis. In Proceedings of the conference on European design automation, 1991. Google ScholarDigital Library
- R. Heckmann, M. Langenbach, S. Thesing, and R. Wilhelm. The influence of processor architecture on the design and the results of WCET tools. Proceedings of the IEEE, 91(7), 2003.Google ScholarCross Ref
- N. Ishiura, H. Sawada, and S. Yajima. Minimization of binary decision diagrams based on exchanges of variables. In ICCAD, pages 472--475, 1991.Google ScholarCross Ref
- R. Jhala and K. L. McMillan. Microarchitecture Verification by Compositional Model Checking. In CAV, pages 396--410, 2001. Google ScholarDigital Library
- D. Kastner, R. Wilhelm, R. Heckmann, M. Schlickling, M. Pister, M. Jersak, K. Richter, and C. Ferdinand. Timing Validation of Automotive Software. In 3rd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISOLA) 2008, Communications in Computer and Information Science (CCIS). Springer, 2008.Google Scholar
- Y.-T. S. Li and S. Malik. Performance analysis of embedded software using implicit path enumeration. In DAC, pages 456--461, 1995. Google ScholarDigital Library
- G. Logothetis and K. Schneider. Exact High Level WCET Analysis of Synchronous Programs by Symbolic State Space Exploration. In DATE, pages 10196--10203, 2003. Google ScholarDigital Library
- T. Lundquist and P. Stenstrom. Timing Anomalies in Dynamically Scheduled Microprocessors. In Proceedings of the 20th IEEE Real-Time Systems Symposium, 1999. Google ScholarDigital Library
- F. Martin. PAG - An Efficient Program Analyzer Generator. STTT, 2(1), 1998.Google Scholar
- F. Martin, M. Alt, R. Wilhelm, and C. Ferdinand. Analysis of Loops. In K. Koskimies, editor, Proceedings of the 7th International Conference on Compiler Construction, LNCS 1383, pages 80--94, Berlin, 1998. Springer. Google ScholarDigital Library
- A. Metzner. Why Model Checking Can Improve WCET Analysis. In CAV, 2004.Google Scholar
- R. Ranjan, A. Aziz, R. Brayton, B. Plessier, and C. Pixley. Efficient BDD Algorithms for FSM Synthesis and Verification, 1995.Google Scholar
- J. Reineke. Caches in WCET Analysis. PhD thesis, Saarland University, 2008.Google Scholar
- R. Rudell. Dynamic variable ordering for ordered binary decision diagrams. In ICCAD '93: Proceedings of the 1993 IEEE/ACM international conference on Computer-aided design, pages 42--47. IEEE Computer Society Press, 1993. Google ScholarDigital Library
- J. Schneider. Combined Schedulability and WCET Analysis for Real-Time Operating Systems. PhD thesis, Saarland University, 2003.Google Scholar
- J. Souyris, E. Le Pavec, G. Himbert, V. Jacgu, G. Borios, and R. Heckmann. Computing the Worst Case Execution Time of an Avionics Program by Abstract Interpretation. In Proceedings of the 5th Intl Workshop on (WCET) Analysis, 2005.Google Scholar
- L. Tan. The Worst-case Execution Time Tool Challenge 2006. International Journal on Software Tools for Technology Transfer (STTT), 11(2):133 -- 152, 2009.Google Scholar
- H. Theiling. ILP-based Interprocedural Path Analysis. In Proceedings of the Workshop on Embedded Software, Grenoble, France, 2002. Google ScholarDigital Library
- H. Theiling. Control Flow Graphs for Real-Time System Analysis. PhD thesis, Saarland University, 2003.Google Scholar
- S. Thesing. Safe and Precise WCET Determination by Abstract Interpretation of Pipeline Models. PhD thesis, Saarland University, 2004.Google Scholar
- S. Thesing, J. Souyris, R. Heckmann, F. Randimbivololona, M. Langenbach, R. Wilhelm, and C. Ferdinand. An Abstract Interpretation-Based Timing Validation of Hard Real-Time Avionics Software. In Proceedings of the International Conference on Dependable Systems and Networks. IEEE Computer Society, 2003.Google ScholarCross Ref
- R. Weicker. Dhrystone benchmark: rationale for version 2 and measurement rules. SIGPLAN Notices, 23(8):49--62, 1988. Google ScholarDigital Library
- R. Wilhelm. Why AI + ILP is good for WCET, but MC is not, nor ILP alone. In In Verification, Model Checking and Abstract Interpretation (VMCAI), LNCS 2937, 2004.Google Scholar
- R. Wilhelm, J. Engblom, A. Ermedahl, N. Holsti, S. Thesing, D. Whalley, G. Bernat, C. Ferdinand, R. Heckmann, F. Mueller, I. Puaut, P. Puschner, J. Staschulat, and P. Stenstrom. The Determination of Worst-Case Execution Times--Overview of the Methods and Survey of Tools. 7(3), 2008. ACM Transactions on Embedded Computing Systems (TECS). Google ScholarDigital Library
Recommendations
The worst-case execution-time problem—overview of methods and survey of tools
The determination of upper bounds on execution times, commonly called worst-case execution times (WCETs), is a necessary step in the development and validation process for hard real-time systems. This problem is hard if the underlying processor ...
Symbolic WCET Computation
Special Issue on MEMCODE 2015 and Regular Papers (Diamonds)Parametric Worst-case execution time (WCET) analysis of a sequential program produces a formula that represents the worst-case execution time of the program, where parameters of the formula are user-defined parameters of the program (as loop bounds, ...
Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints
POPL '77: Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languagesA program denotes computations in some universe of objects. Abstract interpretation of programs consists in using that denotation to describe computations in another universe of abstract objects, so that the results of abstract execution give some ...
Comments