DROPS

Document

DOI: 10.4230/OASIcs.SSV.2011.32

Adaptable Value-Set Analysis for Low-Level Code

Authors: Jörg Brauer, René Rydhof Hansen, Stefan Kowalewski, Kim G. Larsen, and Mads Chr. Olesen

Published in: OASIcs, Volume 24, 6th International Workshop on Systems Software Verification (2012)

Abstract

This paper presents a framework for binary code analysis that uses only SAT-based algorithms. Within the framework, incremental SAT solving is used to perform a form of weakly relational value-set analysis in a novel way, connecting the expressiveness of the value sets to computational complexity. Another key feature of our framework is that it translates the semantics of binary code into an intermediate representation. This allows for a straightforward translation of the program semantics into Boolean logic and eases the implementation efforts, too. We show that leveraging the efficiency of contemporary SAT solvers allows us to prove interesting properties about medium-sized microcontroller programs.

Cite as

Jörg Brauer, René Rydhof Hansen, Stefan Kowalewski, Kim G. Larsen, and Mads Chr. Olesen. Adaptable Value-Set Analysis for Low-Level Code. In 6th International Workshop on Systems Software Verification. Open Access Series in Informatics (OASIcs), Volume 24, pp. 32-43, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{brauer_et_al:OASIcs.SSV.2011.32,
  author =	{Brauer, J\"{o}rg and Hansen, Ren\'{e} Rydhof and Kowalewski, Stefan and Larsen, Kim G. and Olesen, Mads Chr.},
  title =	{{Adaptable Value-Set Analysis for Low-Level Code}},
  booktitle =	{6th International Workshop on Systems Software Verification},
  pages =	{32--43},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-36-1},
  ISSN =	{2190-6807},
  year =	{2012},
  volume =	{24},
  editor =	{Brauer, J\"{o}rg and Roveri, Marco and Tews, Hendrik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SSV.2011.32},
  URN =		{urn:nbn:de:0030-drops-35884},
  doi =		{10.4230/OASIcs.SSV.2011.32},
  annote =	{Keywords: Abstract interpretation, SAT solving, embedded systems}
}

Document

DOI: 10.4230/OASIcs.WCET.2012.1

What is a Timing Anomaly?

Authors: Franck Cassez, René Rydhof Hansen, and Mads Chr. Olesen

Published in: OASIcs, Volume 23, 12th International Workshop on Worst-Case Execution Time Analysis (2012)

Abstract

Timing anomalies make worst-case execution time analysis much harder, because the analysis will have to consider all local choices. It has been widely recognised that certain hardware features are timing anomalous, while others are not. However, defining formally what a timing anomaly is, has been difficult. We examine previous definitions of timing anomalies, and identify examples where they do not align with common observations. We then provide a definition for consistently slower hardware traces that can be used to define timing anomalies and aligns with common observations.

Cite as

Franck Cassez, René Rydhof Hansen, and Mads Chr. Olesen. What is a Timing Anomaly?. In 12th International Workshop on Worst-Case Execution Time Analysis. Open Access Series in Informatics (OASIcs), Volume 23, pp. 1-12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{cassez_et_al:OASIcs.WCET.2012.1,
  author =	{Cassez, Franck and Hansen, Ren\'{e} Rydhof and Olesen, Mads Chr.},
  title =	{{What is a Timing Anomaly?}},
  booktitle =	{12th International Workshop on Worst-Case Execution Time Analysis},
  pages =	{1--12},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-41-5},
  ISSN =	{2190-6807},
  year =	{2012},
  volume =	{23},
  editor =	{Vardanega, Tullio},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2012.1},
  URN =		{urn:nbn:de:0030-drops-35521},
  doi =		{10.4230/OASIcs.WCET.2012.1},
  annote =	{Keywords: Timing anomalies, worst case execution time (WCET), abstractions}
}

Document

DOI: 10.4230/OASIcs.WCET.2010.113

METAMOC: Modular Execution Time Analysis using Model Checking

Authors: Andreas E. Dalsgaard, Mads Chr. Olesen, Martin Toft, René Rydhof Hansen, and Kim Guldstrand Larsen

Published in: OASIcs, Volume 15, 10th International Workshop on Worst-Case Execution Time Analysis (WCET 2010)

Abstract

Safe and tight worst-case execution times (WCETs) are important when scheduling hard real-time systems. This paper presents METAMOC, a modular method, based on model checking and static analysis, that determines safe and tight WCETs for programs running on platforms featuring caching and pipelining. The method works by constructing a UPPAAL model of the program being analysed and annotating the model with information from an inter-procedural value analysis. The program model is then combined with a model of the hardware platform and model checked for the WCET. Through support for the platforms ARM7, ARM9 and ATMEL AVR 8-bit, the modularity and retargetability of the method are demonstrated, as only the pipeline needs to be remodelled. Hardware modelling is performed in a state-of-the-art graphical modelling environment. Experiments on the Mälardalen WCET benchmark programs show that taking caching into account yields much tighter WCETs than without modelling caches, and that METAMOC is a sufficiently fast and versatile approach for WCET analysis.

Cite as

Andreas E. Dalsgaard, Mads Chr. Olesen, Martin Toft, René Rydhof Hansen, and Kim Guldstrand Larsen. METAMOC: Modular Execution Time Analysis using Model Checking. In 10th International Workshop on Worst-Case Execution Time Analysis (WCET 2010). Open Access Series in Informatics (OASIcs), Volume 15, pp. 113-123, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{dalsgaard_et_al:OASIcs.WCET.2010.113,
  author =	{Dalsgaard, Andreas E. and Olesen, Mads Chr. and Toft, Martin and Hansen, Ren\'{e} Rydhof and Larsen, Kim Guldstrand},
  title =	{{METAMOC: Modular Execution Time Analysis using Model Checking}},
  booktitle =	{10th International Workshop on Worst-Case Execution Time Analysis (WCET 2010)},
  pages =	{113--123},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-21-7},
  ISSN =	{2190-6807},
  year =	{2010},
  volume =	{15},
  editor =	{Lisper, Bj\"{o}rn},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2010.113},
  URN =		{urn:nbn:de:0030-drops-28319},
  doi =		{10.4230/OASIcs.WCET.2010.113},
  annote =	{Keywords: WCET analysis, timed automata, model checking, UPPAAL}
}

Search Results

Documents authored by Hansen, René Rydhof

Adaptable Value-Set Analysis for Low-Level Code

Abstract

Cite as

What is a Timing Anomaly?

Abstract

Cite as

METAMOC: Modular Execution Time Analysis using Model Checking

Abstract

Cite as

Thanks for your feedback!

Could not send message