Ansatz zur Modellierung von SPS-Systemen (Teil 1)
3. Analyse und Verbesserung des SPS-Modells
Im vorigen Abschnitt wurde das SPS-Modellierungssystem vorgestellt. Gemäß dieser Strategie können wir das SPS-System in ein formales Modell abstrahieren, um es einer Modellprüfung zu unterziehen. Daher bestimmt die Zuverlässigkeit dieses Modells direkt die Ergebnisse der Modellprüfung. Wenn das Modell das ursprüngliche System nicht vollständig abdeckt (wir bezeichnen es als kleiner als das ursprüngliche System), kann dies dazu führen, dass einige Fehler unentdeckt bleiben; wenn das reale System das Modell vollständig abdeckt, dieses jedoch viele Zustände enthält, die das ursprüngliche System nicht aufweist (wir bezeichnen es als kleiner als das ursprüngliche System), ist das ursprüngliche System zu groß, was zu Fehlern führen kann, die im realen System nicht vorhanden sind. Dies wird als Pseudofehler bezeichnet. Es sind also zwei Modellierungsstrategien erforderlich.
Erstens sollten wir, um alle Fehler im System zu finden, ein Modell erstellen, das groß genug ist, um alle Systeme mit ursprünglichen Zuständen abzudecken; zweitens sollte das Modell so nah wie möglich am realen System sein. Dies wird nicht nur den Zustandsraum verkleinern, sondern auch die Effizienz verbessern. Auf der Grundlage dieser Anforderungen werden wir das Zeitintervallmodell analysieren.
Satz 1: Wenn das Zeitintervallmodell die Eigenschaften erfüllt, erfüllt auch das reale SPS-Systemmodell diese Eigenschaften. Die Richtigkeit von Satz 1 lässt sich aus der Beziehung zwischen den beiden Modellen ableiten. Das bedeutet, dass alles, was im realen Modell geschieht, im Zeitintervallmodell enthalten ist; das Zeitintervallmodell ist also umfassender als das reale Modell. Wenn man mithilfe des Zeitintervallmodells kein Gegenbeispiel finden kann, lässt sich die Korrektheit des realen SPS-Modells nachweisen; findet man hingegen ein Gegenbeispiel, lässt sich nicht feststellen, ob das reale SPS-System Fehler aufweist. Das heißt, die Umkehrung von Satz 1 ist falsch. Es ist dann ein manueller Eingriff erforderlich, um das Gegenbeispiel zu analysieren und festzustellen, ob es sich um einen Scheinfehler handelt.
Mit der Strategie der Zeitintervallmodellierung lässt sich ein zusammengefasstes PLC-Modell erstellen, und viele auf NuSMV basierende Studien nutzen ebenfalls Strategien, die dem Zeitintervallmodell ähneln, um PLC-Systeme zu simulieren. Das “Zeitintervallmodell” weicht jedoch stark vom realen Modell ab und muss verbessert werden. Diese Abweichung besteht darin, dass das “Zeitintervallmodell” die Eigenschaften der SPS hinsichtlich der Hochgeschwindigkeitsabtastung und der Langsamabtastung gleichzeitiger Entitäten nicht widerspiegelt. Das heißt, alle Veränderungen in der Umgebung sollten von der Hochgeschwindigkeits-SPS erfasst werden, doch das Zeitintervallmodell ignoriert die Hochgeschwindigkeitsmerkmale der SPS, sodass Veränderungen in der externen Umgebung möglicherweise nicht erfasst werden. Als Reaktion auf die oben genannten Probleme und unter Berücksichtigung der physikalischen Eigenschaften der externen Hochgeschwindigkeitsabtastung und der langsamen Parallelität wird die Zeitintervall-Modellierungsstrategie durch Hinzufügen eines Benachrichtigungs-Wartemechanismus verbessert. Basierend auf dem Intervallmodell muss jede parallele Zustandsentität nach Abschluss der Übertragung blockiert werden und an einer bestimmten Stelle warten. Erst wenn die SPS-Steuerung mindestens einmal vollständig gescannt hat, wird der Benachrichtigungs-Warte-Mechanismus
Die parallel laufende Instanz löscht den Block und setzt ihre Arbeit fort. Anschließend ist die Übertragung abgeschlossen. Der Ablauf, wie die parallel laufende Instanz die Migration über den Mechanismus der ausstehenden Benachrichtigungen abschließt, ist in Abbildung 2 dargestellt:
t0: Die Übertragung beginnt, wird angehalten und die SPS-Steuerung wird benachrichtigt.
t1-tm: Die SPS führt m-mal einen vollständigen Durchlauf durch (m in
Zumindest.
tm 1: Die parallel laufende Entität empfängt die Benachrichtigung von der SPS, und die Übertragung ist abgeschlossen.
Dieser Mechanismus stellt sicher, dass jede Zustandsänderung einer parallel laufenden Entität von der SPS-Steuerung mindestens einmal erfasst werden kann.
Satz 2
Nach Hinzufügen des Mechanismus für wartende Benachrichtigungen wird das Modell zu einer Teilmenge des Zeitintervallmodells. exist
Gleichzeitig kann das Modell auch alle Situationen des realen Modells abdecken. Mit anderen Worten: Wenn ein Modell einen Mechanismus für das Warten auf Benachrichtigungen hinzufügt, der den Attributen entspricht, entspricht auch das reale SPS-Systemmodell diesen Attributen. Der Nachweis von Satz 2 unter Verwendung von Satz 1 erfolgt in ähnlicher Weise. Anhand von Satz 2 lässt sich erkennen, dass das Mechanismusmodell auch nach Hinzufügen der Benachrichtigungswartung weiterhin gute Eigenschaften aufweist. Wie bereits erwähnt, gelten für abstrakte Systemmodelle zwei Anforderungen: Erstens muss das reale System vollständig abgedeckt sein, und zweitens muss das Modell dem realen System so nahe wie möglich kommen. Mit dem ersten Satz soll bewiesen werden, dass das Zeitintervallmodell das reale System umfasst. Solange Modellprüfungswerkzeuge verwendet werden, um nachzuweisen, dass das abstrakte Modell bestimmte Eigenschaften erfüllt, erfüllen auch die realen Eigenschaften des Systems diese. Dieses Modell ist jedoch nicht exakt gleich dem realen Modell; es sollte wesentlich umfangreicher sein als das reale Modell. Im Vergleich zu Zeitintervallmodellen verringert dieses Modell den Abstand zwischen realen Systemen weiter und reduziert so die Wahrscheinlichkeit, dass Fehlalarme erkannt werden, erheblich.
Ein Modellprüfungswerkzeug liefert ein Gegenbeispiel, das gegen die Eigenschaft des Systems verstößt; es lässt sich leicht manuell feststellen, ob ein Gegenbeispiel in einem realen System zutrifft oder nicht. Wenn der Fehler im ursprünglichen System tatsächlich vorliegt, finden wir ein Gegenbeispiel. Andernfalls liegt der Fehler darin, dass das abstrakte Modell umfangreicher ist als das reale System, was einen Scheinfehler darstellt. Obwohl dieses Zeitintervallmodell dem ursprünglichen System nicht vollständig entspricht, können wir anhand dieses Modells beurteilen, ob ein System eine bestimmte Eigenschaft erfüllt, und falls nicht, ein konkretes Gegenbeispiel finden (es sind jedoch weitere Überprüfungen erforderlich, um festzustellen, ob es sich um einen Scheinfehler handelt). Das Modell ist vor allem deshalb nicht mit dem ursprünglichen System äquivalent, weil es im tatsächlichen System viele Faktoren gibt, die schwer zu modellieren sind und von denen einige zu Fehlern führen können. Würden alle Faktoren modelliert, würde dies zur Erstellung eines riesigen Modells führen, das sich nicht überprüfen lässt oder schlichtweg nicht implementierbar ist. Das Zeitintervallmodell abstrahiert Schlüsselfaktoren aus dem realen System und modelliert diese, wodurch der Zustandsraum erheblich verkleinert und die Zeitkomplexität reduziert wird. Gleichzeitig nähert sich das Modell durch den Mechanismus der Benachrichtigungswartung dem realen System an, was nicht nur die Zeitkomplexität verringert, sondern auch die zuvor erwähnten Pseudofehler reduziert.
Die NuSMV-Prüfung wird auf der Grundlage des oben erstellten Modells durchgeführt. Wir haben eine Reihe von Konvertierungsregeln formuliert, um das oben genannte Modell in die Eingabesprache von SPIN, Promela, zu übertragen. Auch die Systemattribute müssen in Promela übersetzt werden. SPIN führt diese zusammen und führt anschließend die Erkennung durch. Die Sprache PROMELA ist eine C-ähnliche Sprache, und beide Sprachen sind semantisch ähnlich. Daher geben wir lediglich einige Beispiele, um die grundlegenden Konzepte der Übersetzung zu veranschaulichen. 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 mithilfe von Logik zu.
Zähle alle Eingangsanschlüsse. Das ist die Übersetzung.
SPS-Netzwerkverfahren.
Modellprüfung bei SPS (Teil 3)
