Towards Formally Verifiable WCET Analysis for a Functional Programming Language

Authors Kevin Hammond, Christian Ferdinand, Reinhold Heckmann, Roy Dyckhoff, Martin Hofman, Steffen Jost, Hans-Wolfgang Loidl, Greg Michaelson, Robert Pointon, Norman Scaife, Jocelyn Sérot, Andy Wallace



PDF
Thumbnail PDF

File

OASIcs.WCET.2006.677.pdf
  • Filesize: 271 kB
  • 6 pages

Document Identifiers

Author Details

Kevin Hammond
Christian Ferdinand
Reinhold Heckmann
Roy Dyckhoff
Martin Hofman
Steffen Jost
Hans-Wolfgang Loidl
Greg Michaelson
Robert Pointon
Norman Scaife
Jocelyn Sérot
Andy Wallace

Cite AsGet BibTex

Kevin Hammond, Christian Ferdinand, Reinhold Heckmann, Roy Dyckhoff, Martin Hofman, Steffen Jost, Hans-Wolfgang Loidl, Greg Michaelson, Robert Pointon, Norman Scaife, Jocelyn Sérot, and Andy Wallace. Towards Formally Verifiable WCET Analysis for a Functional Programming Language. In 6th International Workshop on Worst-Case Execution Time Analysis (WCET'06). Open Access Series in Informatics (OASIcs), Volume 4, pp. 1-6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)
https://doi.org/10.4230/OASIcs.WCET.2006.677

Abstract

This paper describes ongoing work aimed at the construction of formal cost models and analyses to yield verifiable guarantees of resource usage in the context of real-time embedded systems. Our work is conducted in terms of the domain-specific language Hume, a language that combines functional programming for computations with finitestate automata for specifying reactive systems. We outline an approach in which high-level information derived from source-code analysis can be combined with worst-case execution time information obtained from high quality abstract interpretation of low-level binary code.
Keywords
  • Worst-case execution time
  • functional programming
  • Hume
  • cost model
  • asynchronous
  • finite state machine

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
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