1 Search Results for "Maroneze, Andr�"


Document
A Formally Verified WCET Estimation Tool

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

Published in: OASIcs, Volume 39, 14th International Workshop on Worst-Case Execution Time Analysis (2014)


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.

Cite as

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)


Copy BibTex To Clipboard

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

  • Refine by Classification

  • Refine by Keyword
  • 1 CompCert C Compiler
  • 1 Formal Verification
  • 1 WCET Estimation

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2014

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