Programmnetzlisten: Ein formales Modell für die Verifikation von Hardwarenaher Software in Eingebetteten Systemen
- 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.