Links und Funktionen
Sprachumschaltung

Navigationspfad
You are here: Home / Publikationen / Towards Formally Verifiable WCET Analysis for a Functional Programming Language


Inhaltsbereich

Kevin Hammond, Christian Ferdinand, Reinhold Heckmann, Roy Dyckhoff, Martin Hofmann, Steffen Jost, Hans-Wolfgang Loidl, Greg Michaelson, Robert F Pointon, Norman Scaife, Jocelyn Sérot, and Andy Wallace (2006)

Towards Formally Verifiable WCET Analysis for a Functional Programming Language

In: 6th Intl. Workshop on Worst-Case Execution Time (WCET) Analysis, July 4, 2006, Dresden, Germany, ed. by Frank Mueller, vol. 4, Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany. OASICS.

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.

Document Actions


Funktionsleiste