SD_GF_Echtzeit_Nov_2013

Soliman, D.; Frey, G.: Verifikation und Validierung sicherheitsgerichteter SPS-Programme. Proceedings of the GI-Fachtagung Echtzeit 2013, Boppard, Germany, Nov. 2013.

Kurzfassung

Funktionale Sicherheit nach IEC 61508 umzusetzen ist heutzutage eine der größten Herausforderungen im Design von Automatisierungssystemen. Viele dieser Systeme werden mittels einer Speicherprogrammierbaren Steuerung (SPS) realisiert, welche nach IEC 61131-3 erstellte Steuerungssoftware ausführt. PLCopen, eine Nutzerorganisation mit Fokus auf IEC 61131, spezifizierte in diesem Kontext eine Bibliothek von Funktionsblöcken (FB) zur Verwendung in sicherheitsrelevanten Anwendungen. Dennoch müssen mithilfe dieser Bibliothek erstellte Sicherheitsanwendungen hinsichtlich gegebener Sicherheits-Spezifikationen überprüft werden. Diese Arbeit präsentiert eine Methodik zur Verifikation und Validierung von SPS-Sicherheitsanwendungen, welche aus Funktionsblöcken der PLCopen-Bibliothek erstellt werden. Um formale Analyseansätze verwenden zu können, wird die Sicherheitsanwendung zunächst in ein System aus Modellen zeitbehafteter Automaten überführt. Das entstandene formale Modell kann durch den UPPAAL-Modelchecker formal verifiziert und simulativ validiert werden. Zur einfacheren Anwendbarkeit der vorgestellten Methodik wird die Überführung der PLCopen-Sicherheitsanwendung in zeitbehaftete Automaten nach UPPAAL automatisiert. Hierzu wird eine Modellbibliothek zeitbehafteter Automaten in UPPAAL definiert und verifiziert, die mit der PLCopen-FB-Bibliothek korrespondiert. Die Überführung in das formale Modell nutzt jene Automaten als Blöcke, zur Automatisierung wurde ein Software-Tool entwickelt. Um den Nachweis von Eigenschaften zu erleichtern wird zudem ein Ansatz zur automatisierten Übertragung von Simulationsszenarien aus der Soft-SPS in den Simulator von UPPAAL vorgeschlagen. Um die Anwendbarkeit der Methodik zu demonstrieren, wird ihr Einsatz bei der sicherheitstechnischen Modernisierung einer Laboranlage beschrieben.