1 Search Results for "Crolard, Tristan"

Document
DOI: 10.4230/OASIcs.WCET.2019.5
WCET of OCaml Bytecode on Microcontrollers: An Automated Method and Its Formalisation

Authors: Steven Varoumas and Tristan Crolard

Published in: OASIcs, Volume 72, 19th International Workshop on Worst-Case Execution Time Analysis (WCET 2019)

Abstract
Considering the bytecode representation of a program written in a high-level programming language enables portability of its execution as well as a factorisation of various possible analyses of this program. In this article, we present a method for computing the worst-case execution time (WCET) of an embedded bytecode program fit to run on a microcontroller. Due to the simple memory model of such a device, this automated WCET computation relies only on a control-flow analysis of the program, and can be adapted to multiple models of microcontrollers. This method evaluates the bytecode program using concrete as well as partially unknown values, in order to estimate its longest execution time. We present a software tool, based on this method, that computes the WCET of a synchronous embedded OCaml program. One key contribution of this article is a mechanically checked formalisation of the aforementioned method over an idealised bytecode language, as well as its proof of correctness.
Cite as

Steven Varoumas and Tristan Crolard. WCET of OCaml Bytecode on Microcontrollers: An Automated Method and Its Formalisation. In 19th International Workshop on Worst-Case Execution Time Analysis (WCET 2019). Open Access Series in Informatics (OASIcs), Volume 72, pp. 5:1-5:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{varoumas_et_al:OASIcs.WCET.2019.5,
  author =	{Varoumas, Steven and Crolard, Tristan},
  title =	{{WCET of OCaml Bytecode on Microcontrollers: An Automated Method and Its Formalisation}},
  booktitle =	{19th International Workshop on Worst-Case Execution Time Analysis (WCET 2019)},
  pages =	{5:1--5:12},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-118-4},
  ISSN =	{2190-6807},
  year =	{2019},
  volume =	{72},
  editor =	{Altmeyer, Sebastian},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2019.5},
  URN =		{urn:nbn:de:0030-drops-107702},
  doi =		{10.4230/OASIcs.WCET.2019.5},
  annote =	{Keywords: Worst-case execution time, microcontrollers, synchronous programming, bytecode, OCaml}
}
  • Refine by Author
  • 1 Crolard, Tristan
  • 1 Varoumas, Steven

  • Refine by Classification
  • 1 Computer systems organization → Embedded software
  • 1 Computer systems organization → Real-time systems

  • Refine by Keyword
  • 1 OCaml
  • 1 Worst-case execution time
  • 1 bytecode
  • 1 microcontrollers
  • 1 synchronous programming

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2019

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact