OASIcs.WCET.2014.11.pdf
- Filesize: 0.52 MB
- 10 pages
Document
A Formally Verified WCET Estimation Tool
Authors
-
Part of:
Volume:
14th International Workshop on Worst-Case Execution Time Analysis (WCET 2014)
Series: Open Access Series in Informatics (OASIcs)
Conference: Workshop on Worst-Case Execution Time Analysis (WCET) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2014-07-08
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)
0PDF Downloads
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.