A Formally Verified WCET Estimation Tool

André Oliveira Maroneze 1 Sandrine Blazy 1 David Pichardie 1 Isabelle Puaut 2
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
2 ALF - Amdahl's Law is Forever
Inria Rennes – Bretagne Atlantique , IRISA-D3 - ARCHITECTURE
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.
Type de document :
Communication dans un congrès
14th International Workshop on Worst-Case Execution Time Analysis, Jul 2014, Madrid, Spain. 2014, 〈http://www.uni-ulm.de/en/in/wcet2014.html〉. 〈10.4230/OASIcs.WCET.2014.11〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01087194
Contributeur : Isabelle Puaut <>
Soumis le : mardi 25 novembre 2014 - 15:21:15
Dernière modification le : mardi 16 janvier 2018 - 15:54:17

Identifiants

Citation

André Oliveira Maroneze, Sandrine Blazy, David Pichardie, Isabelle Puaut. A Formally Verified WCET Estimation Tool. 14th International Workshop on Worst-Case Execution Time Analysis, Jul 2014, Madrid, Spain. 2014, 〈http://www.uni-ulm.de/en/in/wcet2014.html〉. 〈10.4230/OASIcs.WCET.2014.11〉. 〈hal-01087194〉

Partager

Métriques

Consultations de la notice

724