SB_GF_SK_BS_DS_EKA_may_2010

Biallas, S.; Frey, G.; Kowalewski, S.; Schlich, B.; Soliman, D.: Formale Verifikation von Sicherheits-Funktionsbausteinen der PLCopen auf Modell- und Code-Ebene. Proceedings of "11th Fachtagung Entwurf komplexer Automatisierungssysteme (EKA 2010)", ISBN 978-3-940961-41-9, pp. 47-54, Magdeburg, May 2010.

Kurzfassung: Im vorliegenden Beitrag wird der Einsatz formaler Methoden zum Nachweis der Korrektheit von Sicherheitssteuerungen demonstriert. Im Bereich der speicherprogrammierbaren Steuerungen hat die PLCopen Software-Bausteine für Sicherheitssteuerungen spezifiziert. Auf Basis dieser semi-formalen Spezifikationen entwickeln wir sowohl formale Modelle als auch konkrete Implementierungen. Auf beiden Ebenen erfolgt eine Verifikation der spezifizierten Eigenschaften mit jeweils geeigneten Model-Checking-Verfahren und Werkzeugen (Uppaal auf Modellebene sowie [mc]square auf Code-Ebene). Der Beitrag zeigt, wie die beiden Ebenen ineinander greifen und demonstriert, dass durch den vorgestellten Ansatz auch Unklarheiten bzw. Interpretationsspielräume in der semi-formalen Spezifikation aufgedeckt werden können. Das Vorgehen wird exemplarisch am Beispiel eines Notaus-Bausteins demonstriert.

Abstract: This paper demonstrates the use of formal methods to verify the correctness of safety controllers. PLCopen organization specified Function Block software models to be used in Programmable Controllers. Based on these specified semi-formal models, we develop formal models for implementation. On both levels, a verification of the specified properties is applied to the models using different model checking techniques and tools (Uppaal on model level and [mc]square on code level). The paper shows how the two levels interact and demonstrates that, by using the presented method, unclarities especially margin of interpretation in the semi-formal specification can be uncovered. The approach is demonstrated using the emergency stop function block as an example.