Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-26402
Titel: Timing model derivation : pipeline analyzer generation from hardware description languages
Verfasser: Pister, Markus
Sprache: Englisch
Erscheinungsjahr: 2012
Quelle: Zugl. im Buchhandel: Saarbrücken : Pirrot, 2012
SWD-Schlagwörter: VHDL
Worst-Case-Laufzeit
Sicherheitskritisches System
Eingebettetes System
Abstrakte Interpretation
Statische Analyse
Freie Schlagwörter: VHDL
worst-case execution time
safety-critical system
embedded system
abstract interpretation
static analysis
DDC-Sachgruppe: 004 Informatik
Dokumentart : Dissertation
Kurzfassung: 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.
Sicherheits-kritische Systeme unterliegen oft der Einhaltung strikter Laufzeitschranken, weshalb zur Verifikation sichere Obergrenzen der Laufzeit im schlimmsten Fall (WCET) bestimmt werden. Zeitmodelle der analysierten Hardware sind hierbei die Grundlage für auf statischen Analysen basierende Verfahren. Aktuell werden solche Modelle händisch aus Handbüchern extrahiert, ein sehr zeitaufwändiger und fehleranfälliger Prozess. Diese Arbeit schlägt eine Brücke zwischen automatischer Hardware-Synthese und der Entwicklung von WCET-Analysen durch die Einführung eines Ableitungsprozesses von Zeitmodellen aus VHDL-Spezifikationen. Transformationen und Abstraktionen werden zur Komplexitätsreduktion eingesetzt, um die Erzeugung von effizienten und beweisbar korrekten Analysatoren zu ermöglichen. Selbige bedienen sich abstrakter Interpretation von Programmausführungen basierend auf einer Simulations-Semantik. Definierte Arbeitsabläufe zeigen, wie man die Ableitung schrittweise auf VHDL-Modellen umsetzt und dadurch für das Zeitverhalten irrelevante Teile des Modells entfernt. Interval Property Checking gewährleistet hierbei, dass die Transformationen semantik-erhaltend sind. Eine Tool-Implementierung realisiert den vorgestellen Ableitungsprozess und unterstreicht seine Anwendbarkeit auf komplexe industrielle Designs durch experimentelle untersuchungen. Außerdem werden VHDL-Designentscheidungen hinsicht ihres Einflusses auf die Qualität des abgeleiteten Zeitmodells betrachtet.
Link zu diesem Datensatz: urn:nbn:de:bsz:291-scidok-49781
hdl:20.500.11880/26458
http://dx.doi.org/10.22028/D291-26402
ISBN der Druckausgabe: 978-3-937436-40-1
Erstgutachter: Wilhelm, Reinhard
Tag der mündlichen Prüfung: 19-Sep-2012
SciDok-Publikation: 7-Nov-2012
Fakultät: Fakultät 6 - Naturwissenschaftlich-Technische Fakultät I
Fachrichtung: MI - Informatik
Fakultät / Institution:MI - Fakultät für Mathematik und Informatik

Dateien zu dieser Ressource:
Datei Beschreibung GrößeFormat 
Dissertation_Markus_Pister.pdf57,37 MBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.