WCET 06 START ConferenceManager    

PDF download PDF

Towards Formally Verifiable WCET Analysis for a Functional Programming Language

Kevin Hammond, Roy Dyckhoff, Christian Ferdinand, Reinhold Heckmann, Martin Hofmann, Steffen Jost, Hans-Wolfgang Loidl, Greg Michaelson, Robert Pointon, Norman Scaife, Jocelyn Serot and Andy Wallace

WORKSHOP ON WORST-CASE EXECUTION TIME (WCET) ANALYSIS 2006 (WCET 06)
Dresden, Germany, July 4, 2006


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 finite-state 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 abstract interpretation of low-level binary code. This abstract interpretation on the machine-code level is capable of dealing with complex architectural effects including cache and pipeline properties in an accurate way.


  
START Conference Manager (V2.50.1)
Maintainer: igor@gandalf.sssup.it