Modelchecking Speicher-bezogener Eigenschaften für Hardware/Software Codesigns

Hardware/Software-Codesign ermöglicht den integrierten Entwurf von Hardware und Software in einer einzigen Modellierungssprache. In Verbindung mit Transaction Level Modeling kann es verwendet werden, um komplexe Systeme auf verschiedenen Abstraktionsebenen effizient zu modellieren. Derartige Systeme werden häufig in sicherheitskritischen Anwendungen eingesetzt, in denen die Korrektheit entscheidend ist. Insbesondere speicherbezogene Fehler können schwerwiegende Probleme verursachen, da sie zu Deadlocks, Laufzeit- Fehlern oder undefiniertem Systemverhalten führen können. HW/SW Codesign ermöglicht das Testen und Simulieren über den gesamten Entwurfsprozess. Allerdings sind diese Techniken unvollständig und können nie die Abwesenheit von Fehlern sicherstellen. Im Gegensatz dazu können formalen Verifikationstechniken wie Model Checking dazu verwendet werden, die Korrektheit eines Designs zu gewährleisten. Obwohl bereits mehrere Ansätze für die formale Verifikation von HW/SW Codesigns existieren, werden speicherbezogene Konstrukte bisher nur unzureichend berücksichtigt. In dieser Arbeit stellen wir einen Ansatz zum Model Checking von speicherbezogenen Eigenschaften für digitale HW/SW Systeme vor. Dazu verwenden wir die System-Level-Beschreibungssprache SystemC, die als de-facto- Standard für HW/SW Codesign gilt, sowie den weit verbreiteten SystemC Transaction Level Modeling Standard (TLM). Die Hauptidee unseres Ansatzes ist es, eine formale Semantik für die wichtigsten Komponenten des TLMStandards sowie ein formales Speichermodell, welches alle relevanten speicherbezogenen Konstrukte abdeckt, zu erstellen. Wir kombinieren unseren Ansatz mit einer bereits bestehenden Formalisierung der Basis-Konstrukte von SystemC und erstellen Transformationsregeln für die vollautomatische Umwandlung von SystemC/TLM-Designs in semantisch äquivalente Uppaal Timed Automata. Die resultierenden Modelle verwenden wir um mithilfe des Uppaal Model Checkers wichtige speicherbezogene, zeitliche und Sicherheits- sowie Lebendigkeitseigenschaften zu verifizieren. Um die Verifikation zu erleichtern, erstellen wir automatisch TCTL-Formeln, die verwendet werden können, um die Abwesenheit von häufigen Fehlern in Designs zu zeigen. Hierzu gehören speicherbezogene Fehler wie Null Pointer und Array Zugriffe außerhalb der Grenzen sowie die Abwesenheit von Verletzungen von Assertions. Wenn eine Eigenschaft verletzt wird, erzeugt der Uppaal Model Checker ein Gegenbeispiel. Dank unserer strukturerhaltenden Transformation können Fehler leicht per Hand im Ursprungsdesign lokalisiert werden. Für die Anwendbarkeit unseres Ansatzes auf komplexe Designs bieten wir zusätzlich eine Reihe von Optimierungstechniken an. Diese verkleinern den semantischen Zustandsraum und verbessern die Performanz der Verifikation. Die Transformation und die Optimierungstechniken haben wir in einer Toolchain implementiert, die vollautomatisch auf SystemC/TLM Designs angewendet werden kann. Wir evaluieren sowohl die Verifikationsperformanz als auch die Fehlererkennungsmöglichkeiten mit verschiedenen Fallstudien, unter anderem einem industriellen SystemC/TLM Design des AMBA AHB.Hardware/software codesign enables the integrated development of hardware and software in a single design language. In combination with transaction level modeling, it can be used to efficiently model complex systems on different levels of abstraction. As such systems are often used in safety-critical applications, the correctness is crucial to prevent high financial losses or casualties. Especially memory-related errors can cause severe problems as they either result in deadlocks, runtime-errors or undefined system behavior. Although HW/SW codesign usually provides means for testing and simulation during the whole development process, these techniques are incomplete and can never ensure the absence of errors. In contrast, formal verification techniques like model checking can be used to guarantee the correctness of a design. Although there exist several approaches for the formal verification of HW/SW codesigns, memory-related constructs and operations are only insufficiently considered. In this thesis, we present an approach for model checking of memoryrelated properties on digital HW/SW systems. To this end, we focus on the system level description language SystemC, the de facto standard for HW/SW codesign. To support transaction level modeling, we additionally take the widely used SystemC transaction level modeling standard (TLM) into account. The main idea of our approach is to provide a formal semantics for the most relevant parts of the TLM standard and a formal memory model, which captures all relevant memory-related constructs and operations. We combine these with an already existing formalization of the basic SystemC constructs and provide transformation rules to enable the fully automatic transformation of SystemC/TLM designs into semantically equivalent Uppaal timed automata models. On the resulting model, we use the Uppaal model checker to verify important properties, including memory-related properties, timing, liveness and safety properties. To ease this verification, we automatically generate a set of verification properties, which can be used to ensure the absence of many common errors in a given design. This includes memory-related errors like null pointer accesses and array out of bounds accesses on a given design as well as the absence of assertion violations. If a property is violated, the Uppaal model checker generates a counterexample. As our formal semantics for SystemC/TLM is structure-preserving, this counterexample can easily be transferred back to the SystemC/TLM code manually and thereby allows for the localization of detected errors. To enhance the applicability of our approach for complex designs, we provide a set of optimization techniques. These are used to reduce the semantic state space and, thus, yield a better verification performance. We have implemented our transformation and our optimization techniques in a toolchain, which can be applied to SystemC/TLM designs fully automatically. We demonstrate both, the verification performance and the errordetection capabilities of our approach with experimental results from various case studies, including an industrial SystemC/TLM design of the AMBA AHB