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

doi:10.4230/OASIcs.WCET.2006.677

Document

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, Andy Wallace

Part of: Volume: 6th International Workshop on Worst-Case Execution Time Analysis (WCET'06) (WCET 2006)
Part of: Series: Open Access Series in Informatics (OASIcs)
Part of: Conference: Workshop on Worst-Case Execution Time Analysis (WCET)
License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
Publication Date: 2006-08-23

PDF

File

OASIcs.WCET.2006.677.pdf

Filesize: 271 kB
6 pages

Document Identifiers

DOI: 10.4230/OASIcs.WCET.2006.677
URN: urn:nbn:de:0030-drops-6773

Author Details

Kevin Hammond

Christian Ferdinand

Reinhold Heckmann

Roy Dyckhoff

Martin Hofman

Steffen Jost

Hans-Wolfgang Loidl

Greg Michaelson

Robert Pointon

Norman Scaife

Jocelyn Sérot

Andy Wallace

Cite AsGet BibTex

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)
https://doi.org/10.4230/OASIcs.WCET.2006.677

@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}
}

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.

Keywords

Worst-case execution time
functional programming
Hume
cost model
asynchronous
finite state machine

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

PDF Downloads

0

Metadata Views

Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail