License
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.WCET.2006.677
URN: urn:nbn:de:0030-drops-6773
URL: http://drops.dagstuhl.de/opus/volltexte/2006/677/
Go to the corresponding Portal


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
Potpourri

Towards Formally Verifiable WCET Analysis for a Functional Programming Language

pdf-format:
Document 1.pdf (271 KB)


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.

BibTeX - Entry

@InProceedings{hammond_et_al:OASIcs:2006:677,
  author =	{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{\'e}rot and Andy Wallace},
  title =	{{Towards Formally Verifiable WCET Analysis for a Functional Programming Language}},
  booktitle =	{6th International Workshop on Worst-Case Execution Time Analysis (WCET'06)},
  series =	{OpenAccess Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-03-3},
  ISSN =	{2190-6807},
  year =	{2006},
  volume =	{4},
  editor =	{Frank Mueller},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2006/677},
  URN =		{urn:nbn:de:0030-drops-6773},
  doi =		{http://dx.doi.org/10.4230/OASIcs.WCET.2006.677},
  annote =	{Keywords: Worst-case execution time, functional programming, Hume, cost model, asynchronous, finite state machine }
}

Keywords: Worst-case execution time, functional programming, Hume, cost model, asynchronous, finite state machine
Seminar: 6th International Workshop on Worst-Case Execution Time Analysis (WCET'06)
Issue Date: 2006
Date of publication: 23.08.2006


DROPS-Home | Fulltext Search | Imprint Published by LZI