Partner:

Förderung:

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:

Download

Die Verifikationsumgebung besteht aus zwei Komponenten, welche hier heruntergeladen werden können:

Für die Isabelle-Theorien wird Isabelle 2009 benötigt, für das C-Frontend der Haskell-Compiler und Cabal.

Letzte Änderung dieser Seite: 2011-02-16 (Rev. 5580) | Datenschutzerklärung | Impressum