Towards formally verifiable WCET analysis for a functional programming language

Kevin Hammond, Christian Ferdinand, Reinhold Heckmann, Roy Dyckhoff, Martin Hofmann, Steffen Jost, Hans-Wolfgang Loidl, Greg Michaelson, Robert Pointon, Norman Scaife, Jocelyn Sérot, Andy Wallace

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 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.

Original languageEnglish
Title of host publicationProceedings of the 6th International Workshop on Worst-Case Execution Time Analysis
PublisherDagstuhl
ISBN (Print)9783939897033
Publication statusPublished - 2006
Event6th International Workshop on Worst-Case Execution Time Analysis 2006 - Dresden, Germany
Duration: 4 Jul 20064 Jul 2006

Publication series

NameOpenAccess Series in Informatics
PublisherDagstuhl
Volume4
ISSN (Print)2190-6807

Conference

Conference6th International Workshop on Worst-Case Execution Time Analysis 2006
Abbreviated titleWCET 2006
CountryGermany
CityDresden
Period4/07/064/07/06

ASJC Scopus subject areas

  • Geography, Planning and Development
  • Modelling and Simulation

Fingerprint Dive into the research topics of 'Towards formally verifiable WCET analysis for a functional programming language'. Together they form a unique fingerprint.

Cite this