License: 
Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.WCET.2018.2
URN: urn:nbn:de:0030-drops-97481
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/9748/
Asavoae, Mihail ;
Ben Hedia, Belgacem ;
Jan, Mathieu
Formal Executable Models for Automatic Detection of Timing Anomalies
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 |
|
Collection: |
|
18th International Workshop on Worst-Case Execution Time Analysis (WCET 2018) |
|
Issue Date: |
|
2018 |
|
Date of publication: |
|
24.09.2018 |
