3) Menschliche Verhaltensweisen
Definition 2.2. Die Entität "menschliches Verhalten" ist ein Tupel Env=
Verhaltensentitäten des Menschen ähneln Hardware-Entitäten;
Sie haben dieselbe Statusdefinition. Es ist schwierig, menschliches Verhalten zu simulieren, insbesondere wenn an der Entwicklung einer SPS mehrere Personen beteiligt sind. Als Reaktion auf diese Schwierigkeiten sollte die Modellierung menschlichen Verhaltens einen iterativen Prozess anwenden: Zunächst wird mithilfe der Modellvalidierung ein einfaches Verhaltensmodell erstellt; wenn dann kein Gegenbeispiel gefunden wird, wird ein komplexeres Modell erstellt und verifiziert, bis ein Gegenbeispiel gefunden wird oder dessen Auffinden schwieriger wird. Komplex; schließlich wird, falls zuvor kein aussagekräftiges Gegenbeispiel gefunden wurde, ein vollständig zufälliges Modell menschlichen Verhaltens (d. h.: menschliches Verhalten ist ein vollständiger Graph und alle Übergänge sind wahr) zur Verifizierung generiert. Die Verifizierung eines vollständig zufälligen Verhaltens führt jedoch zu einer starken Vergrößerung des Zustandsraums, sodass die Wahl eines geeigneten Modells für menschliches Verhalten eine schwierige Frage bei der Modellierung darstellt. Wenn die menschlichen Eingaben relativ einfach sind, können wir eine vollständig zufällige Verhaltensmodellierung verwenden; andernfalls muss ernsthaft in Betracht gezogen werden, ein vernünftiges Modell für menschliches Verhalten zu erstellen.
Wir modellieren das Verhalten der SPS-Umgebung und der Menschen, und dann modellieren wir die SPS-Steuerung. Die SPS-Steuerung befindet sich beim Drehen in einem Zyklus.
Die SPS liest alle Eingänge vom I-Port.
PLC berechnet alle logischen Einheiten.
PLC setzt alle Q-Ports.
Die Grundeinheit des SPS-Prozesses wird als Netz bezeichnet. Alle Netzwerke werden in nummerierter Reihenfolge für die Einrichtung zur Entwurfszeit ausgeführt.
Das grundlegende Logiknetzwerk der SPS-Steuerung umfasst: S-Flipflop, R-Flipflop, SR-Flipflop, EQ-Flipflop, RS-Flipflop, POS-Steigflankendetektor, NEG-Fallflankendetektor usw. Zur Modellierung des grundlegenden Logiknetzwerks verwenden wir eine direkte Abbildungsstrategie, d. h., das Steuerungsmodell des SPS-Netzwerkverhaltens entspricht vollständig dem logischen Verhalten des Netzwerks. Dabei können S-Flipflops, R-Flipflops, SR-Flipflops, EQ-Flipflops und RS-Flipflops mithilfe von Booleschen Ausdrücken direkt auf ihr Verhalten abgebildet werden.
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 eine Modellprüfung durchzuführen. 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 abdecken kann, es aber viele Zustände enthält, die das ursprüngliche System nicht hat (wir bezeichnen es als kleiner als das Originalsystem), während das Originalsystem groß ist), was zu Fehlern führen kann, die im realen System nicht existieren. Dies wird als Pseudo-Fehler 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 Zustände des Originalsystems abzudecken; zweitens muss 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 das reale SPS-Systemmodell diese ebenfalls. 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 größer als das reale Modell. Wenn man mithilfe des Zeitintervallmodells kein Gegenbeispiel finden kann, kann man die Korrektheit des realen SPS-Modells beweisen; finden wir hingegen ein Gegenbeispiel, können wir 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 den Gegenfall zu analysieren und festzustellen, ob es sich um einen Scheinfehler handelt. Die Zeitintervall-Modellierungsstrategie kann ein zusammengefasstes SPS-Modell liefern, und viele auf NuSMV basierende Studien verwenden ebenfalls Strategien, die dem Zeitintervallmodell ähnlich sind, um SPS-Systeme zu modellieren. Das “Zeitintervallmodell” weicht jedoch stark vom realen Modell ab und muss verbessert werden. Diese Abweichung besteht darin, dass das “Zeitintervallmodell” die Eigenschaften der Hochgeschwindigkeits- und Niedriggeschwindigkeits-Abtastung gleichzeitiger Entitäten durch die SPS nicht widerspiegelt. Das heißt, alle Umgebungsänderungen sollten abgetastet werden
Hochgeschwindigkeits-SPS; das Zeitintervallmodell berücksichtigt jedoch nicht die Hochgeschwindigkeitseigenschaften der SPS, sodass Veränderungen in der äußeren Umgebung möglicherweise nicht erfasst werden. Als Reaktion auf die oben genannten Probleme, unter Berücksichtigung der externen Hochgeschwindigkeitserfassung und der langsamen Parallelität
Die Modellierungsstrategien für physikalische Eigenschaften und Zeitintervalle werden durch die Einführung eines Benachrichtigungs-Warte-Mechanismus verbessert. Basierend auf dem Intervallmodell muss jede Entität im Parallelzustand nach Abschluss der Übertragung gesperrt werden und an einer bestimmten Stelle warten. Erst wenn die SPS-Steuerung mindestens einmal vollständig durchlaufen ist, sendet der Benachrichtigungs-Warte-Mechanismus eine Nachricht an die parallele Entität, um die Sperre aufzuheben und die Arbeit fortzusetzen. Dann ist die Übertragung abgeschlossen. Der Prozess der Migration von Entitäten mit konkurrierendem Zugriff durch den Mechanismus der zeitlosen Wartezeit ist in Abbildung 2 dargestellt:
Dieser Mechanismus stellt sicher, dass die SPS-Steuerung jede Zustandsänderung der parallel laufenden Entitäten mindestens einmal abtastet. Satz 2 Nach Hinzufügen des Benachrichtigungswartemechanismus wird das Modell zu einer Teilmenge des Zeitintervallmodells. Gleichzeitig kann das Modell auch alle Situationen des realen Modells abdecken. Mit anderen Worten: Wenn ein Modell einen Benachrichtigungswartemechanismus hinzufügt, der den Attributen entspricht, entspricht auch das reale SPS-Systemmodell diesen Attributen.
Der Beweis von Satz 2 unter Verwendung von Satz 1 verläuft ähnlich. Anhand von Satz 2 lässt sich erkennen, dass das Mechanismusmodell auch nach Hinzufügen der Benachrichtigungswarteschlange weiterhin gute Eigenschaften aufweist. Wie bereits erwähnt, müssen abstrakte Systemmodelle zwei Anforderungen erfüllen: Erstens muss das reale System vollständig abgedeckt sein, und zweitens muss das Modell dem realen System so nahe wie möglich kommen. Die erste Aussage soll beweisen, dass das Zeitintervallmodell das reale System umfasst. Solange Modellprüfungswerkzeuge verwendet werden, um zu beweisen, dass das abstrakte Modell bestimmte Eigenschaften erfüllt, werden auch die realen Eigenschaften des Systems diese erfüllen. Dieses Modell ist jedoch nicht exakt gleich dem realen Modell, sondern sollte wesentlich umfangreicher sein als das reale Modell.
Im Vergleich zu Zeitintervallmodellen verringert dieses Modell die Diskrepanz zu realen Systemen weiter und reduziert so die Wahrscheinlichkeit, dass Scheinfehler 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 existiert, finden wir ein Gegenbeispiel. Andernfalls liegt der Fehler daran, dass das abstrakte Modell größer 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 wenn ja, können wir 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 unmöglich zu überprüfen oder schlichtweg unmöglich zu implementieren wäre. Das Zeitintervallmodell abstrahiert Schlüsselfaktoren aus dem realen System und modelliert diese, wodurch der Zustandsraum erheblich verkleinert und die Zeitkomplexität reduziert wird.
Gleichzeitig wird durch den Mechanismus der Benachrichtigungswarteschlange,
Das Modell nähert sich dem realen System an, was nicht nur die Zeitkomplexität verringert, sondern auch die zuvor erwähnten Pseudofehler reduziert.
