Ansätze für die Modellierung von Streckeninformationen zur Verifikation im Steuerungsentwurf

Abstract

Während der Entwicklung von automatisierten Anlagen ist die Spezifikation der Steuerungslogik ein wichtiger Schritt. Um diesen Prozess mit formalen Methoden zu unterstützen, kann die Steuerungslogik zunächst mithilfe eines formalen Modells spezifiziert werden, was eine formale Verifikation ermöglicht. In einem Vorgängerbeitrag der Autoren wurde eine solche Verifikation vorgestellt, die es ermöglicht, GRAFCET-Spezifikationen zu analysieren. In diesem Beitrag wird dieses Konzept um die Modellierung von Streckeninformationen erweitert. Die Modellierung von Streckeninformationen ermöglicht eine genauere Verifikation und in Teilen eine Reduktion des Zustandsraums. Anhand eines durchgängigen Beispiels werden zwei Ansätze für die Modellierung von Streckeninformationen vorgestellt und verglichen: die Modellierung mittels Invarianten und die Modellierung mittels GRAFCET. Bei der Modellierung mittels GRAFCET wird gezeigt, wie neben dem Verhalten der Steuerstrecke auch zusätzliche Eigenschaften des kombinierten Verhaltens modelliert werden können, wie beispielsweise die korrekte Abarbeitung des SPS-Zyklus. Um diese zusätzlichen Eigenschaften anwenderfreundlich modellieren zu können, wird eine Erweiterung von GRAFCET vorgestellt und gezeigt, wie dieses Konzept zur Modellierung von Streckeninformationen in die bereits vorgestellte Werkzeugkette zur Verifikation von GRAFCET-Spezifikationen integriert werden kann.