2026-07-23T05:16:53Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:677 2024-03-06T10:28:24Z ddc:004 open_access

Towards Formally Verifiable WCET Analysis for a Functional Programming Language Hammond, Kevin Ferdinand, Christian Heckmann, Reinhold Dyckhoff, Roy Hofman, Martin Jost, Steffen Loidl, Hans-Wolfgang Michaelson, Greg Pointon, Robert Scaife, Norman Sérot, Jocelyn Wallace, Andy Worst-case execution time functional programming Hume cost model asynchronous finite state machine 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Kevin Hammond and Christian Ferdinand and Reinhold Heckmann and Roy Dyckhoff and Martin Hofman and Steffen Jost and Hans-Wolfgang Loidl and Greg Michaelson and Robert Pointon and Norman Scaife and Jocelyn Sérot and Andy Wallace 2006 Is Part Of OASIcs, Volume 4, 6th International Workshop on Worst-Case Execution Time Analysis (WCET'06) (2006) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/OASIcs.WCET.2006.677 urn:nbn:de:0030-drops-6773 https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2006.677 eng https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode