A Formally Verified WCET Estimation Tool

Authors André Maroneze, Sandrine Blazy, David Pichardie, Isabelle Puaut



PDF
Thumbnail PDF

File

OASIcs.WCET.2014.11.pdf
  • Filesize: 0.52 MB
  • 10 pages

Document Identifiers

Author Details

André Maroneze
Sandrine Blazy
David Pichardie
Isabelle Puaut

Cite As Get BibTex

André Maroneze, Sandrine Blazy, David Pichardie, and Isabelle Puaut. A Formally Verified WCET Estimation Tool. In 14th International Workshop on Worst-Case Execution Time Analysis. Open Access Series in Informatics (OASIcs), Volume 39, pp. 11-20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014) https://doi.org/10.4230/OASIcs.WCET.2014.11

Abstract

The application of formal methods in the development of safety-critical embedded software is recommended in order to provide strong guarantees about the absence of software errors. In this context, WCET estimation tools constitute an important element to be formally verified. We present a formally verified WCET estimation tool, integrated to the formally verified CompCert C compiler. Our tool comes with a machine-checked proof which ensures that its WCET estimates are safe. Our tool operates over C programs and is composed of two main parts, a loop bound estimation and an Implicit Path Enumeration Technique (IPET)-based WCET calculation method. We evaluated the precision of the WCET estimates on a reference benchmark and obtained results which are competitive with state-of-the-art WCET estimation techniques.

Subject Classification

Keywords
  • Formal Verification
  • CompCert C Compiler
  • WCET Estimation

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. R. Amadio, A. Asperti, N. Ayache, B. Campbell, D. P. Mulligan, R. Pollack, Y. Régis-Gianas, C. S. Coen, and I. Stark. Certified complexity. Procedia CS, 7:175-177, 2011. Google Scholar
  2. M. Berkelaar, K. Eikland, and P. Notebaert. lpsolve : Open source (Mixed-Integer) Linear Programming system. URL: http://lpsolve.sourceforge.net.
  3. F. Besson, T. Jensen, D. Pichardie, and T. Turpin. Certified result checking for polyhedral analysis of bytecode programs. In TGC, pages 253-267. Springer, 2010. Google Scholar
  4. S. Blazy, V. Laporte, A. Maroneze, and D. Pichardie. Formal verification of a C value analysis based on abstract interpretation. In SAS, LNCS, pages 324-344. Springer, 2013. Google Scholar
  5. S. Blazy, A. Maroneze, and D. Pichardie. Formal verification of loop bound estimation for WCET analysis. In VSTTE 2013, LNCS. Springer, 2013. Google Scholar
  6. Coq development team. The Coq proof assistant. http://coq.inria.fr, 1989-2014.
  7. A. Ermedahl, C. Sandberg, J. Gustafsson, S. Bygde, and B. Lisper. Loop bound analysis based on a combination of program slicing, abstract interpretation, and invariant analysis. In WCET, 2007. Google Scholar
  8. J. Gustafsson, A. Betts, A. Ermedahl, and B. Lisper. The Mälardalen WCET benchmarks: Past, present and future. In WCET, pages 137-147, 2010. Google Scholar
  9. R. Heckmann and C. Ferdinand. aiT: worst case execution time prediction by static program analysis. In IFIP Congress Topical Sessions, pages 377-384, 2004. Google Scholar
  10. X. Leroy. Formal verification of a realistic compiler. CACM, 52(7):107-115, 2009. Google Scholar
  11. Y. T. S. Li and S. Malik. Performance analysis of embedded software using implicit path enumeration. IEEE Trans. on CADICS, 16(12):1477-1487, 1997. Google Scholar
  12. P. Lokuciejewski and P. Marwedel. Worst-Case Execution Time Aware Compilation Techniques for Real-Time Systems. Springer, 2011. Google Scholar
  13. M. de Michiel, A. Bonenfant, H. Cassé, and P. Sainrat. Static loop bound analysis of C programs based on flow analysis and abstract interpretation. In Proc. of ERTSS, pages 161-166. IEEE Computer Society, 2008. Google Scholar
  14. G. Necula. Translation validation for an optimizing compiler. In PLDI, pages 83-94. ACM, 2000. Google Scholar
  15. A. Prantl, M. Schordan, and J. Knoop. TuBound - A Conceptually New Tool for Worst-Case Execution Time Analysis. In WCET, 2008. Google Scholar
  16. Tidorum. Bound-T tool homepage. http://www.bound-t.com, 2010.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail