Towards Formally Verifiable WCET Analysis for a Functional Programming Language
Kevin L Hammond, Christian Ferdinand, Reinhold Heckmann, Roy Dyckhoff, Martin O. Hofmann, Steffen Jost, Hans‐Wolfgang Loidl, Greg Michaelson, Robert F. Pointon, Norman Scaife, Jocelyn Sérot, Wallace, Andy · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2006
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.