skip to main content
10.1145/1629335.1629354acmconferencesArticle/Chapter ViewAbstractPublication PagesesweekConference Proceedingsconference-collections
research-article

Symbolic state traversal for WCET analysis

Published:12 October 2009Publication History

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.

References

  1. AbsInt. aiT WCET Analyzers. http://www.absint.com/ait, 2000.Google ScholarGoogle Scholar
  2. C. Berg. PLRU cache domino effects. In 6th Intl. Workshop on Worst-Case Execution Time (WCET) Analysis. Schloss Dagstuhl, Germany, 2006.Google ScholarGoogle Scholar
  3. M. Berndl, O. Lhotak, F. Qian, L. J. Hendren, and N. Umanee. Points-to analysis using BDDs. In PLDI, pages 103--114, 2003. Google ScholarGoogle ScholarDigital LibraryDigital Library
  4. A. Betts, G. Bernat, R. Kirner, P. Puschner, and I. Wenzel. WCET Coverage for Pipelines. Technical report, 2006.Google ScholarGoogle Scholar
  5. D. Beyer, T. A. Henzinger, R. Jhala, and R. Majumdar. The software model checker Blast. STTT, 9(5-6):505--525, 2007. Google ScholarGoogle ScholarCross RefCross Ref
  6. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  7. R. Bryant. Graph based algorithms for boolean function manipulation. In IEEE Transactions on Computers, 1986. Google ScholarGoogle ScholarDigital LibraryDigital Library
  8. J. Burch, E. Clarke, K. McMillan, D. Dill, and J. Hwang. Symbolic model checking: 1020 states and beyond. IEEE Comp. Soc. Press, 1990.Google ScholarGoogle Scholar
  9. S.-T. Cheng. Compiling Verilog into Automata. Technical report, Electronics Research Lab, Univ. of California, Berkeley, CA 94720, 1994.Google ScholarGoogle Scholar
  10. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  11. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  12. EDN. DSP Benchmarks. In EDN - Electronic Design, Strategy, News, Sept. 1988.Google ScholarGoogle Scholar
  13. J. Engblom. Processor Pipelines and Static Worst-Case Execution Time Analysis. PhD thesis, Uppsala University, 2002.Google ScholarGoogle Scholar
  14. C. Ferdinand. Cache Behavior Prediction for Real-Time Systems. PhD thesis, Saarland University, 1997.Google ScholarGoogle Scholar
  15. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  16. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  17. 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 ScholarGoogle ScholarCross RefCross Ref
  18. N. Ishiura, H. Sawada, and S. Yajima. Minimization of binary decision diagrams based on exchanges of variables. In ICCAD, pages 472--475, 1991.Google ScholarGoogle ScholarCross RefCross Ref
  19. R. Jhala and K. L. McMillan. Microarchitecture Verification by Compositional Model Checking. In CAV, pages 396--410, 2001. Google ScholarGoogle ScholarDigital LibraryDigital Library
  20. 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 ScholarGoogle Scholar
  21. Y.-T. S. Li and S. Malik. Performance analysis of embedded software using implicit path enumeration. In DAC, pages 456--461, 1995. Google ScholarGoogle ScholarDigital LibraryDigital Library
  22. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  23. T. Lundquist and P. Stenstrom. Timing Anomalies in Dynamically Scheduled Microprocessors. In Proceedings of the 20th IEEE Real-Time Systems Symposium, 1999. Google ScholarGoogle ScholarDigital LibraryDigital Library
  24. F. Martin. PAG - An Efficient Program Analyzer Generator. STTT, 2(1), 1998.Google ScholarGoogle Scholar
  25. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  26. A. Metzner. Why Model Checking Can Improve WCET Analysis. In CAV, 2004.Google ScholarGoogle Scholar
  27. R. Ranjan, A. Aziz, R. Brayton, B. Plessier, and C. Pixley. Efficient BDD Algorithms for FSM Synthesis and Verification, 1995.Google ScholarGoogle Scholar
  28. J. Reineke. Caches in WCET Analysis. PhD thesis, Saarland University, 2008.Google ScholarGoogle Scholar
  29. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  30. J. Schneider. Combined Schedulability and WCET Analysis for Real-Time Operating Systems. PhD thesis, Saarland University, 2003.Google ScholarGoogle Scholar
  31. 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 ScholarGoogle Scholar
  32. 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 ScholarGoogle Scholar
  33. H. Theiling. ILP-based Interprocedural Path Analysis. In Proceedings of the Workshop on Embedded Software, Grenoble, France, 2002. Google ScholarGoogle ScholarDigital LibraryDigital Library
  34. H. Theiling. Control Flow Graphs for Real-Time System Analysis. PhD thesis, Saarland University, 2003.Google ScholarGoogle Scholar
  35. S. Thesing. Safe and Precise WCET Determination by Abstract Interpretation of Pipeline Models. PhD thesis, Saarland University, 2004.Google ScholarGoogle Scholar
  36. 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 ScholarGoogle ScholarCross RefCross Ref
  37. R. Weicker. Dhrystone benchmark: rationale for version 2 and measurement rules. SIGPLAN Notices, 23(8):49--62, 1988. Google ScholarGoogle ScholarDigital LibraryDigital Library
  38. 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 ScholarGoogle Scholar
  39. 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 ScholarGoogle ScholarDigital LibraryDigital Library

Recommendations

Comments

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Sign in
  • Published in

    cover image ACM Conferences
    EMSOFT '09: Proceedings of the seventh ACM international conference on Embedded software
    October 2009
    332 pages
    ISBN:9781605586274
    DOI:10.1145/1629335

    Copyright © 2009 ACM

    Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

    Publisher

    Association for Computing Machinery

    New York, NY, United States

    Publication History

    • Published: 12 October 2009

    Permissions

    Request permissions about this article.

    Request Permissions

    Check for updates

    Qualifiers

    • research-article

    Acceptance Rates

    EMSOFT '09 Paper Acceptance Rate33of106submissions,31%Overall Acceptance Rate60of203submissions,30%

    Upcoming Conference

    ESWEEK '24
    Twentieth Embedded Systems Week
    September 29 - October 4, 2024
    Raleigh , NC , USA

PDF Format

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader