A Formally Verified WCET Estimation Tool

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

doi:10.4230/OASIcs.WCET.2014.11

File

OASIcs.WCET.2014.11.pdf

Filesize: 0.52 MB
10 pages

Document Identifiers

DOI: 10.4230/OASIcs.WCET.2014.11
URN: urn:nbn:de:0030-drops-46003

Author Details

André Maroneze

Sandrine Blazy

David Pichardie

Isabelle Puaut

Cite AsGet 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.

Keywords

Formal Verification
CompCert C Compiler
WCET Estimation

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

PDF Downloads

0

Metadata Views

References

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.
M. Berkelaar, K. Eikland, and P. Notebaert. lpsolve : Open source (Mixed-Integer) Linear Programming system. URL: http://lpsolve.sourceforge.net.
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.
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.
S. Blazy, A. Maroneze, and D. Pichardie. Formal verification of loop bound estimation for WCET analysis. In VSTTE 2013, LNCS. Springer, 2013.
Coq development team. The Coq proof assistant. http://coq.inria.fr, 1989-2014.
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.
J. Gustafsson, A. Betts, A. Ermedahl, and B. Lisper. The Mälardalen WCET benchmarks: Past, present and future. In WCET, pages 137-147, 2010.
R. Heckmann and C. Ferdinand. aiT: worst case execution time prediction by static program analysis. In IFIP Congress Topical Sessions, pages 377-384, 2004.
X. Leroy. Formal verification of a realistic compiler. CACM, 52(7):107-115, 2009.
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.
P. Lokuciejewski and P. Marwedel. Worst-Case Execution Time Aware Compilation Techniques for Real-Time Systems. Springer, 2011.
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.
G. Necula. Translation validation for an optimizing compiler. In PLDI, pages 83-94. ACM, 2000.
A. Prantl, M. Schordan, and J. Knoop. TuBound - A Conceptually New Tool for Worst-Case Execution Time Analysis. In WCET, 2008.
Tidorum. Bound-T tool homepage. http://www.bound-t.com, 2010.