DROPS

Document

DOI: 10.4230/OASIcs.WCET.2006.677

Towards Formally Verifiable WCET Analysis for a Functional Programming Language

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

Published in: OASIcs, Volume 4, 6th International Workshop on Worst-Case Execution Time Analysis (WCET'06) (2006)

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.

Cite as

Kevin Hammond, Christian Ferdinand, Reinhold Heckmann, Roy Dyckhoff, Martin Hofman, Steffen Jost, Hans-Wolfgang Loidl, Greg Michaelson, Robert Pointon, Norman Scaife, Jocelyn Sérot, and Andy Wallace. Towards Formally Verifiable WCET Analysis for a Functional Programming Language. In 6th International Workshop on Worst-Case Execution Time Analysis (WCET'06). Open Access Series in Informatics (OASIcs), Volume 4, pp. 1-6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{hammond_et_al:OASIcs.WCET.2006.677,
  author =	{Hammond, Kevin and Ferdinand, Christian and Heckmann, Reinhold and Dyckhoff, Roy and Hofman, Martin and Jost, Steffen and Loidl, Hans-Wolfgang and Michaelson, Greg and Pointon, Robert and Scaife, Norman and S\'{e}rot, Jocelyn and Wallace, Andy},
  title =	{{Towards Formally Verifiable WCET Analysis for a Functional Programming Language}},
  booktitle =	{6th International Workshop on Worst-Case Execution Time Analysis (WCET'06)},
  pages =	{1--6},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-03-3},
  ISSN =	{2190-6807},
  year =	{2006},
  volume =	{4},
  editor =	{Mueller, Frank},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.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}
}

@InProceedings{hammond_et_al:OASIcs.WCET.2006.677,
  author =	{Hammond, Kevin and Ferdinand, Christian and Heckmann, Reinhold and Dyckhoff, Roy and Hofman, Martin and Jost, Steffen and Loidl, Hans-Wolfgang and Michaelson, Greg and Pointon, Robert and Scaife, Norman and S\'{e}rot, Jocelyn and Wallace, Andy},
  title =	{{Towards Formally Verifiable WCET Analysis for a Functional Programming Language}},
  booktitle =	{6th International Workshop on Worst-Case Execution Time Analysis (WCET'06)},
  pages =	{1--6},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-03-3},
  ISSN =	{2190-6807},
  year =	{2006},
  volume =	{4},
  editor =	{Mueller, Frank},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.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}
}

Search Results

Documents authored by Michaelson, Greg

Towards Formally Verifiable WCET Analysis for a Functional Programming Language

Abstract

Cite as

Thanks for your feedback!

Could not send message