TY - GEN
T1 - Towards formally verifiable WCET analysis for a functional programming language
AU - Hammond, Kevin
AU - Ferdinand, Christian
AU - Heckmann, Reinhold
AU - Dyckhoff, Roy
AU - Hofmann, Martin
AU - Jost, Steffen
AU - Loidl, Hans-Wolfgang
AU - Michaelson, Greg
AU - Pointon, Robert
AU - Scaife, Norman
AU - Sérot, Jocelyn
AU - Wallace, Andy
PY - 2006
Y1 - 2006
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84880172938&partnerID=8YFLogxK
M3 - Conference contribution
AN - SCOPUS:84880172938
SN - 9783939897033
T3 - OpenAccess Series in Informatics
BT - Proceedings of the 6th International Workshop on Worst-Case Execution Time Analysis
PB - Dagstuhl
T2 - 6th International Workshop on Worst-Case Execution Time Analysis 2006
Y2 - 4 July 2006 through 4 July 2006
ER -