Hohe Zuverlässigkeit ist der Schlüssel zur Leistung elektrischer Steuergeräte. Die SPS kombiniert Computertechnologie, automatische Steuerungstechnik und Kommunikationstechnologie und ist bei der Automatisierung von Industrieprozessen weit verbreitet. Herkömmliche Überprüfungsmethoden können einigen Anforderungen komplexer SPS-Systeme nicht gerecht werden. In diesem Papier wird eine effiziente Methode zur Modellierung und Überprüfung von SPS-Systemen vorgeschlagen. Um die Hochgeschwindigkeitsleistung der SPS zu gewährleisten, haben wir das "Zeitintervallmodell" und die "Benachrichtigungswartetechnologie" vorgeschlagen. Damit kann der Zustandsraum reduziert werden, und es ist möglich, einige komplexe SPS-Systeme zu verifizieren. Darüber hinaus wurde die Konvertierung des etablierten SPS-Modells in die Promela-Sprache durchgeführt und ein Tool PLC-Checker für die Modellierung und Überprüfung von SPS-Systemen entwickelt. Mit dem PLC-Checker kann man ein klassisches SPS-Beispiel überprüfen und ein Gegenbeispiel finden. Obwohl die Wahrscheinlichkeit, dass dieser Logikfehler auftritt, sehr gering ist, kann er zum Absturz des Systems führen.
1. Einleitung
Eine SPS ist ein automatisches Steuergerät, das logische Eingangssignale von Sensoren, Rechnern oder anderen SPSen empfangen und verarbeitete logische Signale ausgeben kann.
Steuerungsalgorithmen können in Standardsprachen wie Kontaktplan (KOP), strukturierter Text (ST) oder Anweisungsliste (AWL) [1] geschrieben werden.
Die SPS nutzt die programmierbare Sprachtechnologie zur Steuerung großer integrierter Schaltungen und ist in der Industrie weit verbreitet [2]. Da sicherheitskritische Software schwere Schäden an Menschenleben oder Eigentum verursachen kann, ist die Überprüfung sicherheitskritischer Software ein unverzichtbarer Schritt zur Gewährleistung der Softwarequalität. Die derzeitige Methode zur Verifizierung von SPS stützt sich immer noch auf Simulation und Tests. Sie decken jedoch nicht alle möglichen Situationen ab, insbesondere nicht die Frage, ob das Designmodell der SPS den Anforderungen entspricht. Daher wurde die Technologie der Modellprüfung in den SPS-Bereich eingeführt. Die theoretische Analyse und der Entwurf von SPS sind sehr wichtig geworden.
Der erste Schritt bei der SPS-Modellprüfung ist die Erstellung eines SPS-Modells, z. B. die Erstellung eines Modells aus einem Funktionsplan [3]. Das SPS-Modell konzentriert sich auf die Festlegung von Zeitattributen [4]. Es kann mit der Methode der zeitgesteuerten Automaten [5] oder der Methode der Zeitperiodenmodellierung [6] modelliert werden. Daher wird der Zustandsraum des Modells im Vergleich zu einem zeitgesteuerten Automaten reduziert. Unabhängig davon, welche Methode gewählt wird, kann schließlich ein abstraktes Modell erstellt werden [7]. Die Erstellung eines guten abstrakten SPS-Modells hat bei der Inspektion oberste Priorität. Bei der manuellen Modellierung können leicht viele Fehler auftreten, daher ist es sehr wichtig, ein integriertes Modellierungs- und Testwerkzeug zu entwickeln. Dies ist eines der Anliegen dieses Artikels.
Das SPS-Steuerungsprogramm läuft in einem Echtzeit-Betriebssystem (Multi-Task oder Single-Task); dieser Artikel basiert hauptsächlich auf einem SPS-System mit Multi-Task-Scheduling. Abschnitt 2 Der Artikel stellt die Modellierungsmethode des SPS-Systems vor. In Abschnitt 3 werden die Analyse und die Verbesserungen dieses Modells beschrieben, da wir störende Fehler reduzieren müssen. Abschnitt 4 entwirft ein Modellprüfungswerkzeug PLC-Checker, um das erstellte Modell zu prüfen, einschließlich der Einführung der Methode zur Umwandlung des SPS-Programms in die SPIN-Eingabesprache Promela-Code. Schließlich wird ein klassisches SPS-Beispiel zur Überprüfung und ein kritisches Computerbeispiel von PLC-Checker gefunden.
2.PLC-Modellierung*
Diese Arbeit wurde von den interdisziplinären Stiftungen NSFC 60973049, 60635020 und TNList finanziert. Die Modellprüfung gliedert sich in drei Schritte: Modellierung, Eigenschaftsbeschreibung und Überprüfung. Das Wichtigste ist, wie man ein Systemmodell aufbaut. Im System ist die SPS-Steuerung nicht isoliert, sondern hat Wechselwirkungen mit der Arbeitsumgebung, den Fahrern und den Menschen [8]. Daher sollten diese Faktoren ebenfalls modelliert werden. Die Umgebung, die Menschen und die SPS-Steuerung sind logisch unabhängig und parallel zueinander. Darüber hinaus ist die Eingabesprache des Modellprüfers SPIN, Promela, auf die Beschreibung der Gleichzeitigkeit ausgerichtet, so dass wir ausgehend von dieser Idee diese Faktoren in mehrere nebenläufige Prozesse einbauen, um den Prüfungen von SPIN zu entsprechen, die das System ebenfalls genau beschreiben. Zur Vereinfachung der Beschreibung werden sie als nebenläufige Einheiten bezeichnet. SPS-Steuerungen und konkurrierende Entitäten werden in der Abbildungstabelle durch Symbole dargestellt.
Die Symbole des SPS-Systems umfassen I (Eingangsanschluss), Q (Ausgangsanschluss) und M (mittleres Relais). Abbildung 1 ist ein Modelldiagramm des SPS-Systems. Strategie der Intervallmodellierung: Verwendung von Bit-Zuständen, die markieren, welche spezifische gleichzeitige Einheit die gleichzeitige Einheit in dem Zustand darstellt, unabhängig von der Systemuhr. Dadurch können Unterschiede in den Zeitzuständen ignoriert werden, wodurch das SPS-Modell vereinfacht wird.
Die Modellierungsstrategie fügt keine Systemtaktattribute hinzu und entspricht nicht vollständig dem Modell der ursprünglichen SPS. Das liegt vor allem daran, dass durch das Hinzufügen des Systemtakts das SPS-Systemmodell zu groß wird und es kein Modellprüfungswerkzeug gibt, das mit einem so großen Modell umgehen kann. Der Ausgangspunkt für die Modellierung des Zustands ist dies, ohne die Anzahl der SPS-Abtastungen zu berücksichtigen, wenn ein Übergang stattgefunden hat. Unabhängig davon, wie oft Sie die erlebten Übergänge abfragen, werden sie alle in diesem Modell enthalten sein. Mit anderen Worten, das reale Modell wird eine Teilmenge des erstellten Modells (Zeitintervallmodell) sein, denn die reale SPS-Umgebung ist komplex und umfasst eine
Verschiedene Hardware und menschliches Verhalten.die folgenden
Wir werden verschiedene Arten von konkurrierenden Einheiten in der SPS-Umgebung analysieren.
1) Hardware-Einheit
Die Hardware-Einheiten des SPS-Systems sind hauptsächlich einige SPS-gesteuerte Geräte. Der Status dieser Geräte kann als Eingabe für die SPS-Steuerung verwendet werden. Daher ist die Hardware-Entität an ihr zugehöriges I und Q gebunden, und die Hardware hat ihren eigenen Arbeitsablauf, der durch die Hardware-Anforderungen bestimmt wird. Dieser Arbeitsablauf kann in einen Automaten abstrahiert werden. Dieser Automat wird verwendet, um den Arbeitszustand der Hardware zu beschreiben. Definition 2.1. Die Hardware-Entität ist ein Tupel Env =
Das Zustandsübergangsdiagramm der Hardware-Entität basiert auf der Teilung von Symbol I, und das Zeitattribut wird nicht berücksichtigt. Das Zustandsübergangsdiagramm der Hardware-Entität ist eigentlich die Abstraktion der Hardware-Entität, wenn sie ignoriert wird, und die abstrakte Simulation erfordert einen Bezug zur Hardware.
2) Eine einfache Ausgangsentität, die nur an den Q-Port gebunden ist, verwendet den I-Port nicht, was bedeutet, dass die einfache Ausgangsentität kein Zustandsübergangsdiagramm hat. Eine einfache Ausgangsentität ist ein Gerät, das den Arbeitsstatus der SPS anzeigt, ähnlich wie eine Lampe. Die Verwendung einfacher Ausgangsentitäten besteht darin, an den Q-Port zu binden, damit die SPS ihre Logik entwerfen kann.
3) Definition der menschlichen Verhaltensweisen 2.2. Die Entität "menschliches Verhalten" ist ein Tupel Env=
Menschliche Aktionseinheiten sind ähnlich wie Hardware-Entitäten; sie haben die gleiche Zustandsdefinition. Es ist schwierig, menschliches Verhalten zu simulieren, vor allem, wenn die Entwicklung einer SPS eine Reihe von Personen umfasst. Als Reaktion auf diese Schwierigkeiten sollte die Modellierung des menschlichen Verhaltens einen iterativen Prozess annehmen: Zunächst wird ein einfaches Verhaltensmodell mit Hilfe der Modellvalidierung erstellt; wenn dann z. B. kein Zähler gefunden wird, wird ein komplexeres Modell erstellt und validiert,
Bis ein Gegenbeispiel gefunden wird oder es schwierig ist, komplexer zu sein; wenn schließlich kein sinnvolles Gegenbeispiel gefunden wird, wird ein völlig zufälliges menschliches Verhaltensmodell erzeugt (das heißt: menschliches Verhalten ist ein vollständiger Graph
Alle Übertragungen sind echt) zu verifizieren. Die Verifizierung von völlig zufälligem Verhalten führt jedoch zu einer starken Vergrößerung des Zustandsraums, so dass die Wahl eines geeigneten menschlichen Verhaltensmodells ein schwieriger Punkt bei der Modellierung ist. Wenn der menschliche Input relativ einfach ist, können wir die Modellierung von völlig zufälligem Verhalten verwenden, andernfalls müssen Sie ernsthaft in Betracht ziehen, ein vernünftiges Modell des menschlichen Verhaltens 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 logische Operationsnetzwerk des PLC-Controllers umfasst: S-Flip-Flop, R-Flip-Flop, SR-Flip-Flop, EQ-Flip-Flop, RS-Flip-Flop, POS-Detektor für steigende Flanken, NEG-Detektor für fallende Flanken usw. Für die Modellierung der grundlegenden logischen Operationen des Netzwerks verwenden wir eine direkte Abbildungsstrategie, d. h. das Netzwerkverhalten des SPS-Steuermodells und das logische Verhalten des Netzwerks sind völlig gleichwertig. Flip-Flops, R-Flip-Flops, SR-Flip-Flops, EQ-Flip-Flops und RS-Flip-Flops können direkt auf ihr Verhalten mit Hilfe boolescher Ausdrücke abgebildet werden.