TY  - THES
T1  - Timing model derivation : pipeline analyzer generation from hardware description languages
T3  - Zugl. im Buchhandel: Saarbrücken : Pirrot, 2012
A1  - Pister,Markus
Y1  - 2012/11/07
N2  - Safety-critical systems are forced to finish their execution within strict deadlines so that worst-case execution time (WCET) guarantees are a crucial part of their verification. Timing models of the analyzed hardware form the basis for static analysis-based approaches like the aiT WCET analyzer. Currently, timing models are hand-crafted based on frequently incorrect documentation causing the process to be error-prone and time-consuming. This thesis bridges the gap between automatic hardware synthesis and WCET analysis development by introducing a process for the derivation of timing models from VHDL specifications. We propose a set of transformations and abstractions to reduce the hardware design's complexity enabling the generation of efficient and provably correct WCET analyzers. They employ an abstract interpretation-based simulation of program executions based on a defined abstract simulation semantics. We have defined workflow patterns showing how to gradually apply the derivation process to VHDL models, thereby removing timing-irrelevant constructs. Interval property checking is used to validate the transformations. A further contribution of this thesis is the implementation of a tool set that realizes the introduced derivation process and shows its applicability to non-trivial industrial designs in experimental evaluations. Influences on design choices to the quality of the derived timing model are presented building an informal predictability notion for VHDL.
KW  - VHDL
KW  - Worst-Case-Laufzeit
KW  - Sicherheitskritisches System
KW  - Eingebettetes System
KW  - Abstrakte Interpretation
KW  - Statische Analyse
CY  - Saarbrücken
PB  - Universitäts- und Landesbibliothek
SN  - 978-3-937436-40-1 
AD  - Postfach 151141, 66041 Saarbrücken
UR  - http://scidok.sulb.uni-saarland.de/volltexte/2012/4978
ER  -