Timing model derivation : pipeline analyzer generation from hardware description languages
Markus Pister · Publications of the UdS (Saarland University) · 2012
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 fur auf statischen Analysen basierende Verfahren. Aktuell werden solche Modelle handisch aus Handbuchern extrahiert, ein sehr zeitaufwandiger und fehleranfalliger Prozess. Diese Arbeit schlagt eine Brucke zwischen automatischer Hardware-Synthese und der Entwicklung von WCET-Analysen durch die Einfuhrung eines Ableitungsprozesses von Zeitmodellen aus VHDL-Spezifikationen. Transformationen und Abstraktionen werden zur Komplexitatsreduktion eingesetzt, um die Erzeugung von effizienten und beweisbar korrekten Analysatoren zu ermoglichen. Selbige bedienen sich abstrakter Interpretation von Programmausfuhrungen basierend auf einer Simulations-Semantik. Definierte Arbeitsablaufe zeigen, wie man die Ableitung schrittweise auf VHDL-Modellen umsetzt und dadurch fur das Zeitverhalten irrelevante Teile des Modells entfernt. Interval Property Checking gewahrleistet 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. Auserdem werden VHDL-Designentscheidungen hinsicht ihres Einflusses auf die Qualitat des abgeleiteten Zeitmodells betrachtet.