Bernard Schmidt

• In dieser Arbeit wird ein formales Modell zur Beschreibung von hardwarenaher Software vorgestellt: Die Programmnetzliste. Die Programmnetzliste (PN) besteht aus Instruktionszellen die in einem gerichteten azyklischen Graph verbunden sind und dabei alle Ausführungspfade des betrachteten Programms beinhaltet. Die einzelnen Instruktionszellen repräsentieren eine Instruktion oder eine Instruktionssequenz. Die PN verfügt über eine explizite Darstellung des Programmablaufs und eine implizite Modellierung des Datenpfads und ist als Modell für die Verifikation von Software nutzbar. Die Software wird dabei auf Maschinencode-Level betrachtet. Die Modellgenerierung besteht aus wenigen und gut automatisierbaren Schritten. Als Grundlage dient ein – ggf. unvollständiger – Kontrollfluss Graph (CFG), der aus der Software generiert werden kann. Die Modellgenerierung besteht aus zwei Schritten. Der erste Schritt ist die Erzeugung des expliziten Programmablaufs, indem der CFG abgerollt wird. Dabei wird ein sogenannter Execution-Graph (EXG) erzeugt, der alle möglichen Ausführungspfade des betrachteten Programms beinhaltet. Um dieses Modell so kompakt wie möglich zu halten, werden unterschiedliche Techniken verwendet – wie das Zusammenführen gemeinsamer Pfade und das Erkennen von “toten” Verzweigungen im Programm, die an der entsprechenden Stelle niemals ausgeführt werden. Im Anschluss wird im zweiten Schritt der Execution-Graph in die Programmnetzliste (PN) übersetzt. Dabei werden alle Knoten im EXG durch eine entsprechende Instruktionszelle ersetzt. Die Kanten des Graphen entsprechen dabei dem Programmzustand. Der Programmzustand setzt sich aus den Variablen im Speicher wie auch dem Architekturzustand des unterliegenden Prozessors zusammen. Ergänzt wird der Programmzustand in der Programmnetzliste um ein sogenanntes Active-Bit, welches es ermöglicht den aktiven Pfad in der Netzliste zu markieren. Das ist notwendig, da die Software immer nur einen Pfad gleichzeitig ausführen kann, aber die PN alle möglichen Pfade beinhaltet. Auf der Programmnetzliste können dann mit Hilfe von Hardware Property Checkern basierend auf BMC oder IPC diverse Eigenschaften bewiesen werden. Zusätzlich wird die Programmnetzliste um die Fähigkeit zur Interruptmodellierung erweitert.