DROPS

Document

DOI: 10.4230/OASIcs.WCET.2018.2

Formal Executable Models for Automatic Detection of Timing Anomalies

Authors: Mihail Asavoae, Belgacem Ben Hedia, and Mathieu Jan

Published in: OASIcs, Volume 63, 18th International Workshop on Worst-Case Execution Time Analysis (WCET 2018)

Abstract

A timing anomaly is a counterintuitive timing behavior in the sense that a local fast execution slows down an overall global execution. The presence of such behaviors is inconvenient for the WCET analysis which requires, via abstractions, a certain monotony property to compute safe bounds. In this paper we explore how to systematically execute a previously proposed formal definition of timing anomalies. We ground our work on formal designs of architecture models upon which we employ guided model checking techniques. Our goal is towards the automatic detection of timing anomalies in given computer architecture designs.

Cite as

Mihail Asavoae, Belgacem Ben Hedia, and Mathieu Jan. Formal Executable Models for Automatic Detection of Timing Anomalies. In 18th International Workshop on Worst-Case Execution Time Analysis (WCET 2018). Open Access Series in Informatics (OASIcs), Volume 63, pp. 2:1-2:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{asavoae_et_al:OASIcs.WCET.2018.2,
  author =	{Asavoae, Mihail and Ben Hedia, Belgacem and Jan, Mathieu},
  title =	{{Formal Executable Models for Automatic Detection of Timing Anomalies}},
  booktitle =	{18th International Workshop on Worst-Case Execution Time Analysis (WCET 2018)},
  pages =	{2:1--2:13},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-073-6},
  ISSN =	{2190-6807},
  year =	{2018},
  volume =	{63},
  editor =	{Brandner, Florian},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2018.2},
  URN =		{urn:nbn:de:0030-drops-97481},
  doi =		{10.4230/OASIcs.WCET.2018.2},
  annote =	{Keywords: timing anomalies, predictability, formal methods, model checking}
}

Search Results

Documents authored by Ben Hedia, Belgacem

Formal Executable Models for Automatic Detection of Timing Anomalies

Abstract

Cite as

Thanks for your feedback!

Could not send message