Verifikation einer Funktionsblockbibliothek für die Prozessautomatisierung

Produktbeschreibung

Aus dem Inhalt

Kurzfassung

Um einen hohen Automatisierungsgrad erreichen zu können, wird der Einsatz von Software in der Prozessautomatisierung immer wichtiger. Allerdings hat Software bis heute nicht das Maß an Verlässlichkeit erreicht, das zu ihrem Einsatz in sicherheitsgerichteten Automatisierungssystemen erforderlich ist. Von den bisherigen Forschungsergebnissen ausgehend erscheint dieses Maß jedoch erreichbar, wenn zum Programmentwurf eine grafische Programmiersprache in Verbindung mit einer vorab verifizierten Funktionsblockbibliothek genutzt wird. Gleichwohl existieren bislang weder eine entsprechende Bibliothek noch geeignete Methoden, um eine solche überhaupt realisieren zu können. Folgerichtig werden in der vorliegenden Arbeit zunächst die in der Informatik bereits vorhandenen Verifikationstechniken beleuchtet. Dabei wird mit dem quasiempirischen Beweis eine Strategie identifiziert, die wegen ihrer Ausrichtung am menschlichen Denken geeignet ist, auch eine umfangreiche Funktionsblockbibliothek zu verifizieren. Um diese Strategie nutzen zu können, werden verschiedene Modelle und Verifikationstaktiken erarbeitet. Im Zuge dessen entsteht insbesondere ein Modell, das Funktionsblöcke als synchrone endliche Zustandsautomaten beschreibt und so die getrennte Verifikation von Ausgabe und Zustand des jeweiligen Bausteins möglich macht. Auf dieser Grundlage wird schließlich eine 44 Funktionsblöcke umfassende, auf der Richtlinie VDI/VDE 3696 basierende Bibliothek spezifiziert, in der Programmiersprache Strukturierter Text implementiert und mittels quasiempirischem Beweis verifiziert. Dabei werden Funktionsblockentwurf und Verifikation stets parallel durchgeführt, wodurch sich strukturell sehr einfache Implementierungen und Beweise ergeben. Um den praktischen Nutzen der Bibliothek zum Entwurf verlässlicher.

Inhaltsverzeichnis

Kurzfassung VII
Abstract VIII
1 Einführung 1
1.1 Ursachen und Folgen von Fehlern in rechnergestützten Automatisierungssystemen
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1
1.2 Wege zu verlässlicher Automatisierungssoftware . . . . . . . . . . . . . . . 3
1.3 Ziel und Aufbau der vorliegenden Arbeit . . . . . . . . . . . . . . . . . . . 6
2 Verlässliche rechnergestützte Automatisierungssysteme durch Verifikation 8
2.1 Von der Spezifikation zum Korrektheitsbeweis . . . . . . . . . . . . . . . . 8
2.2 Vorhandene Methoden zur Softwareverifikation . . . . . . . . . . . . . . . . 10
2.2.1 Vollständiger Test . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10
2.2.2 Symbolische Ausführung . . . . . . . . . . . . . . . . . . . . . . . . 11
2.2.3 Formale Methoden . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
2.2.4 Diversitäre Rückübersetzung . . . . . . . . . . . . . . . . . . . . . . 13
2.2.5 Quasiempirischer Beweis . . . . . . . . . . . . . . . . . . . . . . . . 15
2.3 Eignungsbewertung der vorhandenen Methoden . . . . . . . . . . . . . . . 16
2.4 Zusammenfassung des Kapitels . . . . . . . . . . . . . . . . . . . . . . . . 21
3 Die Richtlinie VDI/VDE 3696 als Basis der Bibliothek 22
3.1 Analyse des Funktionsumfangs der Richtlinie VDI/VDE 3696 . . . . . . . 22
3.1.1 Logische Operationen . . . . . . . . . . . . . . . . . . . . . . . . . . 25
3.1.2 Arithmetische Operationen . . . . . . . . . . . . . . . . . . . . . . . 26
3.1.3 Auswahlfunktionen . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
3.1.4 Relationale Operationen . . . . . . . . . . . . . . . . . . . . . . . . 29
3.1.5 Mathematische Grundfunktionen . . . . . . . . . . . . . . . . . . . 29
3.1.6 Prozesseingabe und -ausgabe . . . . . . . . . . . . . . . . . . . . . . 30
3.1.7 Zähler, Zeitgeber, mono- und bistabile Elemente . . . . . . . . . . . 30
3.1.8 Dateneingabe und -speicherung . . . . . . . . . . . . . . . . . . . . 30
3.1.9 Dynamische Elemente und Regler . . . . . . . . . . . . . . . . . . . 32
3.2 Funktionsumfang der Bibliothek für die Prozessautomatisierung . . . . . . 32
3.3 Zusammenfassung des Kapitels . . . . . . . . . . . . . . . . . . . . . . . . 35
4 Programmzerlegung in Verifikationsebenen als Verifikationstaktik 36
4.1 Intrinsisch sichere Programmentwürfe durch Funktionspläne . . . . . . . . 37
4.2 Verifikation des Zeitverhaltens von Echtzeitsystemen . . . . . . . . . . . . 38
4.3 Modellierung von Funktionsblöcken als Zustandsautomaten . . . . . . . . . 40
4.4 Zusammenfassung des Kapitels . . . . . . . . . . . . . . . . . . . . . . . . 43
5 Umsetzung verifizierbarer Funktionsblöcke in der Sprache Strukturierter Text 44
5.1 Relevante Spracheigenschaften und geeignete Verifikationstaktiken . . . . . 44
5.1.1 Programmorganisationseinheiten . . . . . . . . . . . . . . . . . . . 45
5.1.2 Variablenarten . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
5.1.3 Datentypen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
5.1.4 Operatoren . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
5.1.5 Kontrollstrukturen . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
5.2 Verifikation von ST-Funktionsbausteinen mit dem Automatenmodell . . . . 52
5.3 Zusammenfassung des Kapitels . . . . . . . . . . . . . . . . . . . . . . . . 56
6 Eine verifizierte Funktionsblockbibliothek für die Prozessautomatisierung 57
6.1 Schema der Bibliothekseinträge . . . . . . . . . . . . . . . . . . . . . . . . 57
6.1.1 Allgemeine und spezielle Spezifikation . . . . . . . . . . . . . . . . 57
6.1.2 Beschreibung der Programmierschnittstelle . . . . . . . . . . . . . . 59
6.1.3 Implementierung der speziellen Spezifikation . . . . . . . . . . . . . 60
6.1.4 Korrektheitsbeweis der Implementierung . . . . . . . . . . . . . . . 61
6.2 Logische Operationen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61
6.3 Arithmetische Operationen . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
6.4 Auswahlfunktionen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76
6.5 Relationale Operationen . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83
6.6 Mathematische Grundfunktionen . . . . . . . . . . . . . . . . . . . . . . . 96
6.7 Zähler, Zeitgeber, mono- und bistabile Elemente . . . . . . . . . . . . . . . 105
6.8 Dateneingabe und -speicherung . . . . . . . . . . . . . . . . . . . . . . . . 130
6.9 Dynamische Elemente und Regler . . . . . . . . . . . . . . . . . . . . . . . 146
6.10 Zusammenfassung des Kapitels . . . . . . . . . . . . . . . . . . . . . . . . 164
7 Applikationsbeispiel eines verlässlichen PID-Reglers 165
7.1 Umsetzung des Reglers als Funktionsplan . . . . . . . . . . . . . . . . . . . 165
7.2 Einsatz des Reglers in einer Datenverarbeitungsanlage nach Halang und
Sniezek . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 167
7.2.1 Rückübersetzung der Funktionsblöcke am Beispiel der Multiplikation 169
7.2.2 Rückübersetzung des Funktionsplans . . . . . . . . . . . . . . . . . 174
7.3 Zusammenfassung des Kapitels . . . . . . . . . . . . . . . . . . . . . . . . 177
8 Fazit und Ausblick 178
Literatur 181

Kurzfassung
Um einen hohen Automatisierungsgrad erreichen zu können, wird der Einsatz von Software in der Prozessautomatisierung immer wichtiger. Allerdings hat Software bis heute nicht das Maß an Verlässlichkeit erreicht, das zu ihrem Einsatz in sicherheitsgerichteten Automatisierungssystemen erforderlich ist. Von den bisherigen Forschungsergebnissen ausgehend erscheint dieses Maß jedoch erreichbar, wenn zum Programmentwurf eine grafische Programmiersprache in Verbindung mit einer vorab verifizierten Funktionsblockbibliothek
genutzt wird.
Gleichwohl existieren bislang weder eine entsprechende Bibliothek noch geeignete Methoden, um eine solche überhaupt realisieren zu können. Folgerichtig werden in der vorliegenden Arbeit zunächst die in der Informatik bereits vorhandenen Verifikationstechniken beleuchtet. Dabei wird mit dem quasiempirischen Beweis eine Strategie identifiziert, die wegen ihrer Ausrichtung am menschlichen Denken geeignet ist, auch eine umfangreiche Funktionsblockbibliothek zu verifizieren. Um diese Strategie nutzen zu können, werden verschiedene
Modelle und Verifikationstaktiken erarbeitet. Im Zuge dessen entsteht insbesondere ein Modell, das Funktionsblöcke als synchrone endliche Zustandsautomaten beschreibt und so die getrennte Verifikation von Ausgabe und Zustand des jeweiligen Bausteins möglich macht. Auf dieser Grundlage wird schließlich eine 44 Funktionsblöcke umfassende, auf der Richtlinie VDI/VDE 3696 basierende Bibliothek spezifiziert, in der Programmiersprache Strukturierter Text implementiert und mittels quasiempirischem Beweis verifiziert. Dabei
werden Funktionsblockentwurf und Verifikation stets parallel durchgeführt, wodurch sich strukturell sehr einfache Implementierungen und Beweise ergeben. Um den praktischen Nutzen der Bibliothek zum Entwurf verlässlicher Automatisierungssoftware nachzuweisen, wird deren Verwendung abschließend am Beispiel eines idealen PID-Reglers demonstriert. In diesem Kontext wird auch die leichte Verifizierbarkeit der
maschinensprachlichen Übersetzung durch diversitäre Rückübersetzung gezeigt, sowohl in Bezug auf die zugrunde liegenden Funktionsblöcke als auch hinsichtlich des resultierenden Programms. Somit schafft diese Arbeit die Grundlage zum Entwurf sicherheitstechnisch abnehmbarer rechnergestützter Automatisierungssysteme. Gleichzeitig können die vorgestellten Konzepte und Methoden aber auch in Anwendungen außerhalb der Prozessautomatisierung
zu erhöhter Verlässlichkeit von Software beitragen. Denn sie lassen sich beispielsweise ebenso auf die in kommerziellen Applikationen weitverbreiteten objektorientierten Programmiersprachen übertragen.

Keywords: Funktionsblock, Bibliothek, Prozessautomatisierung,