Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH scholarly article en Asavoae, Mihail; Ben Hedia, Belgacem; Jan, Mathieu http://www.dagstuhl.de/oasics License
when quoting this document, please refer to the following
DOI:
URL:

; ;

Formal Executable Models for Automatic Detection of Timing Anomalies

pdf-format:


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.

BibTeX - Entry

@InProceedings{asavoae_et_al:OASIcs:2018:9748,
  author =	{Mihail Asavoae and Belgacem Ben Hedia and Mathieu Jan},
  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 =	{OpenAccess Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-073-6},
  ISSN =	{2190-6807},
  year =	{2018},
  volume =	{63},
  editor =	{Florian Brandner},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/9748},
  doi =		{10.4230/OASIcs.WCET.2018.2},
  annote =	{Keywords: timing anomalies, predictability, formal methods, model checking}
}

Keywords: timing anomalies, predictability, formal methods, model checking
Seminar: 18th International Workshop on Worst-Case Execution Time Analysis (WCET 2018)
Issue date: 2018
Date of publication: 2018


DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI