Towards formally verifiable resource bounds for real-time embedded systems

This paper describes ongoing work aimed at the construction of formal cost models and analyses that are capable of producing verifiable guarantees of resource usage (space, time and ultimately power consumption) in the context of realtime 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 describe 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. 1