Die SAMS Verifikationsumgebung
Die SAMS Verifikationsumgebung ist ein auf dem Theorembeweiser Isabelle aufbauendes Werkzeug zur funktionalen Verifikation von MISRA-C-Programmen, welches im Rahmen des Projektes SAMS entwickelt worden ist. Der C-Quellcode wird mit Spezifikationen annotiert, wie beispielsweise Funktionen mit Vor- und Nachbedingungen. Die Korrektheit wird mit der Verifikationsumgebung interaktiv bewiesen.
Die Verifikationsumgebung besteht aus einem Frontend, welches die Einhaltung der MISRA-Programmierrichtlinien überprüft und den C-Quellcode nach Isballe übersetzt, und einem semantischen Backend in Isabelle, welches die Einhaltung der annotierten Bedingungen beweist. Folgende Abbildung zeigt den Datenfluss (generierte Dateien sind grau hinterlegt):
Um mehr über die Verifikationsumgebung zu erfahren:
- sehen Sie ein Demonstrations-Video über die Verifikationsumgebung an einem einfachen Beispiel im Einsatz, oder
- lesen Sie das Papier Certifiable specification and verification of C programs (erschienen auf der FM'09), oder
- studieren Sie das Referenzhandbuch, welches Syntax und Bedeutung der Annotationen erläutert, sowie die unterstützten Konstrukte der Sprache C.
Download
Die Verifikationsumgebung besteht aus zwei Komponenten, welche hier heruntergeladen werden können:
- Die Isabelle-Theorien, welche den eigentlichen Korrektheitsbeweis ermöglichen, und
- das C-Frontend, welches annotierte C-Programme nach Isabelle übersetzt.
