4. Modellprüfung der SPS
SPS kommen in vielen Anwendungsbereichen zum Einsatz und umfassen zahlreiche Geräte; sie stellen ein umfangreiches Forschungsgebiet dar. Bei jeder Arbeit mit SPS sind unterschiedliche Geräte und Personen beteiligt, sodass das SPS-System parallel arbeitet. Gleichzeitig ist ein
Sollten im SPS-System Fehler auftreten, die schwer zu finden sind, sind diese hauptsächlich auf logische Konstruktionsfehler zurückzuführen, nicht jedoch auf Rechenfehler. Daher konzentrieren wir uns auf den logischen Ablauf des SPS-Prüfprogramms, und diese Logik kann vollständig
Beschreibung der Bitlogik. Um das SPS-Programmmodell zu vereinfachen und den Schwerpunkt auf die Modellprüfung zu legen, nehmen wir daher folgende Einstellungen vor:
Eine SPS ist ein logisches Steuerungsprogramm, und alle Steuerungsvariablen haben nur zwei Zustände: 0 und 1;
SPS-Programme laufen in einer parallelen Umgebung. In diesem Fall ist es wahrscheinlicher, dass die SPS-Programmierung Fehler enthält, die nicht leicht zu finden sind. Angesichts der oben genannten Eigenschaften verwenden wir das Modellprüfungswerkzeug SPIN (unser PLC-Checker implementiert NuSMV ebenfalls auf der Grundlage des oben erstellten Modells) zur Überprüfung. Wir haben eine Reihe von Konvertierungsregeln formuliert, um das oben genannte Modell in die Eingabesprache von SPIN, Promela, zu übertragen. Auch Systemattribute müssen in Promela übersetzt werden. SPIN führt diese zusammen und führt anschließend die Fehlererkennung durch. Die Sprache Promela ist eine C-ähnliche Sprache, und beide Sprachen sind semantisch ähnlich. Sehen wir uns daher einige Beispiele an
Vermittelt grundlegende Konzepte der Übersetzung. Ausführliche Informationen zur Sprache PROMELA finden Sie unter www.spinroot.com. Wir stellen die drei Teile der PROMELA-Datei als Eingabe für SPIN vor.
1) SPS-Steuerungscode
Eine SPS-Steuerung besteht aus mehreren Netzwerken.
Der Code für die SPS-Steuerung wird ebenfalls aus dem Netzwerk generiert. Natürlich sollten Sie zuvor die benötigten Variablen deklarieren. Jedes Netzwerk verfügt über Eingangs- und Ausgangsanschlüsse, und jeder Anschluss kann durch einen booleschen Ausdruck dargestellt werden. Den Wert des Ausgangsanschlusses weisen wir über Logik zu.
Zähle alle Eingangsanschlüsse. Dies ist die Übersetzung.
SPS-Netzwerkverfahren.
Hier ist ein Beispiel für die Umwandlung eines SR-Netzwerks:
if ::Exp(R) == 1 -> Q = 0; ::else -> if ::Exp(S) == 1 -> Q = 1; ::else -> überspringen; fi; fi; /* Exp(S) ist der Boolesche Ausdruck des Ports S, Exp(R) ist der Boolesche Ausdruck des Ports R, Q ist der Ausgangsport */
2) Kodex für parallel existierende Rechtsträger
Wir gehen davon aus, dass jede parallele Entität einen eigenständigen Prozess darstellt, unabhängig vom menschlichen Verhalten oder von der Ausrüstung. Diese Prozesse teilen sich Variablen mit dem SPS-Steuerungsprozess. Dies ist erforderlich, um die Parallelität des Systems zu gewährleisten. Im zweiten Teil dieses Artikels haben wir erläutert, dass alle parallelen Entitäten als Automaten modelliert werden. Ein Automat bedeutet den Übergang von einem Zustand in einen anderen. Wir verwenden I-Ports, um den Zustand der Entität zu bilden. Verwenden Sie goto-Anweisungen als Sprünge (genau wie in der Assemblersprache). Ein einfaches Beispiel sieht wie folgt aus:
atomic { if :: Q1 -> {IB, goto StateB} :: Q2 -> {IC, goto StateC} fi;} /* StateA ist die Bezeichnung für Zustand A, Q1 und Q2 sind die Übergangsbedingungen, IB dient dazu, den Zustandswert auf den Wert von Zustand B zu setzen, goto StateB bedeutet „Sprung zu Zustand B“ */
3) Eigenschaftscode
Eigenschaften sind Regeln, die das SPS-System einhalten muss. Als Eingabeformat verwenden wir LTL-Formeln (Linear Time Logic). Aufgrund des Funktionsprinzips von SPIN sollten wir die gegenteilige Eigenschaft formulieren. SPIN wird feststellen, dass unsere Fall-Eigenschaft eintritt, was ein Gegenbeispiel darstellen sollte. Wir können die LTL-Formel nicht direkt schreiben, sondern verwenden das Makro “ing”. Zunächst sollten wir alle Aussagen in Makros in LTL definieren (z. B. #define p i5 == 0), dann verwenden wir die definierten Aussagen, um LTL-Formeln zu bilden. SPIN kann LTL-Formeln mithilfe des Befehls „SPIN-f“ automatisch in PRO-MELA-Code umwandeln (weitere Details finden Sie im SPIN-Handbuch).
4) Mechanismus für ausstehende Benachrichtigungen
In der Diskussion zur Modellierung empfehlen wir, keinen Zeitwarte-Mechanismus hinzuzufügen. Dieser Mechanismus muss sich auch im Code widerspiegeln. Die konkrete Umsetzung besteht darin, eine Bit-Variable jedes Nicht-SPS-Prozesses (mit Ausnahme aller SPS-Prozesssteuerungen) als Signal zu kennzeichnen. Wenn der Automat in einen Zustand mit einer Zustandsbezeichnung wechselt, wird die Signalvariable auf 0 gesetzt, und die nächste Zuweisung erfordert, dass diese Variable den Wert 1 hat, um fortzufahren. Dieser Vorgang wird durch die Syntaxmerkmale von PROMELA gewährleistet. Im SPS-Prozess gibt es keine derartige Einschränkung. Stattdessen kann der SPS-Prozess diese Variablen auf 1 setzen und so sicherstellen, dass jeder Schritt durch mindestens einen SPS-Durchlauf abgeschlossen werden muss. Dies wird als Benachrichtigungs-Wartemechanismus bezeichnet.
Wenn wir die vier oben genannten Schritte befolgen, erhalten wir eine vollständige SPIN-Eingabedatei für unser System. Anschließend können wir das Modell mit SPIN überprüfen. Eine Schritt-für-Schritt-Anleitung zur Überprüfung des SPIN-Modells finden Sie im SPIN-Handbuch (unter www.spinroot.com). SPIN gibt an, ob ein Gegenbeispiel gefunden wurde. Wir können die oben erwähnte, von SPIN bereitgestellte Tracking-Datei theoretisch analysieren. Mithilfe dieses Erkennungsmechanismus haben wir ein Tool zur Modellprüfung namens „PLC-Checker“ entwickelt. Es unterstützt die Erstellung visueller Modelle und die Durchführung von Prüfungen und kann eine einfache Analyse der Ergebnisse liefern. Natürlich sollte das gefundene Gegenbeispiel manuell überprüft werden, um festzustellen, ob es sich um ein echtes Gegenbeispiel handelt. Mit Hilfe von Trail-Dateien ist dies jedoch keine besonders schwierige Aufgabe. Wir haben zudem erfolgreich einige PLC-Checker eingesetzt (siehe nächster Abschnitt). Im klassischen Lehrbuchbeispiel wurde ein Gegenbeispiel gefunden. Obwohl die Wahrscheinlichkeit für Gegenbeispiele sehr gering ist, treten sie doch auf und können schwerwiegende Folgen haben. Dieses Tool belegt zudem die Richtigkeit und Gültigkeit der in diesem Artikel dargelegten Theorie.
5. PLC-Checker ausführen
Wir werden die Wirksamkeit des PLC-Checkers bei der Überprüfung des Zwei-Gate-Kanalmodells auf folgende Weise demonstrieren. Zwei Türdurchgänge dienen dazu, den Raum von der Außenwelt abzuschotten.
Durch die Eingabe des Kontaktplan-Diagramms und der parallelen Entitäten in das Tool – was der Definition der Eigenschaften entspricht – führen wir eine Überprüfung durch. Abbildung 3 zeigt die Ergebnisse. Wie wir sehen können, liegt im Ergebnis ein Fehler vor. Dies wird durch die Überprüfung der Hinweise als echtes Gegenbeispiel zur manuellen Archivierung belegt. Das heißt, unser Mechanismus ist bei der Überprüfung solcher SPS-Programme wirksam.
6. Abschließend
In diesem Beitrag untersuchen wir die Modellierungs- und Prüftheorie von SPSen unter Verwendung formaler Methoden. Anhand der Anforderungen werden die Merkmale der SPS-Modellierung analysiert und ein Modell für parallele Entitäten mittels einer Zeitintervallstrategie erstellt. Anschließend beweisen wir, dass das Zeitintervallmodell eine Obermenge der SPS-Systeme darstellt, und reduzieren das Modell durch Hinzufügen eines zeitunabhängigen Wartemechanismus. Dadurch wird zudem sichergestellt, dass alle Änderungen am System von der SPS-Steuerung erfasst werden können. Wir haben festgestellt, dass sich Fehler in einem System durch die Untersuchung seiner Gegenbeispiele aufspüren lassen. Abschließend wird die Verwendung von SPIN zur Modellprüfung vorgestellt. Zudem enthält der Beitrag eine entsprechende Einführung in das Modellprüfungswerkzeug PLC-Checker. Derzeit ist der Mechanismus noch sehr unvollkommen, beispielsweise hinsichtlich seiner Funktionsweise als Timer. Er bietet jedoch große und einzigartige Vorteile bei der Lösung von Problemen der Zustandserkundung. Wir beschäftigen uns weiterhin aktiv mit diesen Fragestellungen.
