The beta version of DROPS 2 is now publicly available! Check this page out at DROPS 2 now!


License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
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://dagstuhl.sunsite.rwth-aachen.de/volltexte/2006/677/
Go to the corresponding OASIcs Volume 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:
WCET_Hammond.677.pdf (0.3 MB)

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 =		{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
Collection: 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 | Privacy Published by LZI