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

Pavlović, Olivera

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.

Programmable logic controllers (PLCs) are electronic systems used for different industrial control tasks. The development of PLCs in the last years has made it possible to apply PLCs for tasks of higher complexity. Many systems based on these controllers are safety-related systems. The certification of which entails a great effort. Therefore, there is a big demand for tools to analyze PLC applications and providing a proof of correctness for these systems. Within the scope of this thesis it is examined, how a proof of correctness of safety-related systems based on PLCs can be provided. The IEC has proposed five languages for PLC programming. The verification of one of the languages, the graphical PLC programming language Function Block Diagram (FBD), has been examined in this thesis. The specific PLC used as case study for this thesis is a Siemens SIMATIC S7. The automation of the verification process is an important precondition for efficient involvement of the verification in the development of PLCs. For this purpose a suitable verification method is model checking. In the process each state of the model is explored and checked, whether the designated property is fulfilled in the state or not. A method for automated transformation of an FBD program into a model suitable for model checking has been proposed in this work. The application of the method to the field of rail automation is described by a case study. In the case study the specification has also been automatically transformed into an appropriate logic. Therewith the whole verification process has been fully automated. This work has been developed within the scope of Rail Automation Graduate School (RA:GS!) by Siemens AG, Industry Sector at Brunswick. The gained results provide an evidence, that formal methods have the potential for commercial use in the industrial field.

Vorschau

Zitieren

Zitierform:

Pavlović, Olivera: Formale Verifikation von Software für speicherprogrammierbare Steuerungen mittels Model Checking. 2009.

Zugriffsstatistik

Gesamt:
Volltextzugriffe:
Metadatenansicht:
12 Monate:
Volltextzugriffe:
Metadatenansicht:

Details anzeigen

Rechte

Nutzung und Vervielfältigung:
Alle Rechte vorbehalten

Export