License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.WCET.2014.11
URN: urn:nbn:de:0030-drops-46003
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2014/4600/
Go to the corresponding OASIcs Volume Portal

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

A Formally Verified WCET Estimation Tool

pdf-format:
3.pdf (0.5 MB)

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.

BibTeX - Entry

@InProceedings{maroneze_et_al:OASIcs:2014:4600,
  author =	{Andr{\'e} Maroneze and Sandrine Blazy and David Pichardie and Isabelle Puaut},
  title =	{{A Formally Verified WCET Estimation Tool}},
  booktitle =	{14th International Workshop on Worst-Case Execution Time Analysis},
  pages =	{11--20},
  series =	{OpenAccess Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-69-9},
  ISSN =	{2190-6807},
  year =	{2014},
  volume =	{39},
  editor =	{Heiko Falk},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2014/4600},
  URN =		{urn:nbn:de:0030-drops-46003},
  doi =		{10.4230/OASIcs.WCET.2014.11},
  annote =	{Keywords: Formal Verification, CompCert C Compiler, WCET Estimation}
}

Keywords: Formal Verification, CompCert C Compiler, WCET Estimation
Collection: 14th International Workshop on Worst-Case Execution Time Analysis
Issue Date: 2014
Date of publication: 08.07.2014

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI