Towards Formally Verifiable WCET Analysis for a Functional Programming Language
(2006)6th Intl WORKSHOP ON WORST-CASE EXECUTION TIME (WCET) ANALYSIS
Dresden, Germany, July 4, 2006
http://moss.csc.ncsu.edu/~mueller/wcet06
in conjunction with the
18th Euromicro Intl Conference on Real-Time Systems
Dresden, Germany, July 5 - 7, 2006
http://moss.csc.ncsu.edu/~mueller/wcet06/accepted/1.html.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.