Formale Verifikation von Software für speicherprogrammierbare Steuerungen mittels Model Checking

Speicherprogrammierbare Steuerungen (SPS) sind elektronische, für verschiedene Steuerungsaufgaben in industrieller Umgebung eingesetzte Systeme. Parallel zur allgemeinen Entwicklung der Technik werden auch SPS weiterentwickelt und für immer komplexere Aufgaben eingesetzt. Da heutzutage viele Systeme mit Sicherheitsverantwortung auf SPS basieren, ist es vor dem Einsatz wichtig feststellen zu können, ob sie fehlerfrei funktionieren oder nicht. Im Rahmen dieses Dissertationsprojekts wird untersucht, wie die Korrektheit einer Anwendungsapplikation für sicherheitsrelevante Systeme auf Basis einer SPS bewiesen werden kann. Das internationale Normungsgremium für Normen im Bereich Elektrotechnik und Elektronik hat fünf Sprachen für die SPS-Programmierung vorgeschlagen. In der vorliegenden Arbeit wird das Verifikationspotenzial einer dieser Sprachen, der graphischen SPS-Programmiersprache Funktionsbaustein-Sprache (FBS), untersucht. Konkret wird hier mit der SIMATIC S7-Steuerung gearbeitet, deren entsprechende Sprache als Funktionsplan (FUP) bezeichnet ist. Eine wichtige Voraussetzung für die effiziente Einbindung der Verifikation in die SPS-Entwicklung ist die Automatisierung des Verifikationsprozesses. Eine dafür geeignete Verifikationsmethode ist Model Checking. Dabei werden alle Zustände des Modells untersucht und es wird überprüft, ob in jedem Zustand die gewünschte Eigenschaft erfüllt ist. In dieser Arbeit wird der in einer SPS-Programmiersprache erstellte Code automatisch zum Modell transformiert. Es wird eine Fallstudie vorgestellt, mit der die Anwendung der Methode im Bereich der Eisenbahnautomatisierung beschrieben wird. In der Fallstudie wird zusätzlich auch die Spezifikation automatisch in eine geeignete Logik überführt. Damit wird der ganze Prozess der formalen Verifikation vollautomatisiert. Diese Arbeit entstand im Rahmen des Graduiertenkollegs Rail Automation Graduate School (RA:GS!) der Siemens AG, Industry Sector in Braunschweig. Die erzielten Ergebnisse weisen nach, dass formale Verifikation das Potenzial zum kommerziellen Einsatz in industrieller Umgebung besitzt.