High reliability is key to the performance of electrical control equipment. PLC combines computer technology, automatic control technology, and communication technology and is widely used in the automation of industrial processes. Traditional verification methods cannot meet some requirements of complex PLC systems. In this paper, an efficient PLC system modeling and verification method is proposed. In order to ensure the high-speed performance of PLC, we proposed the “time interval model” and “notification waiting” technology. It can reduce the state space and make it possible to verify some complex PLC systems. In addition, the conversion from the established PLC model to the Promela language was obtained, and a tool, PLC-Checker, for PLC system modeling and checking was designed. Use PLC-Checker to check a classic PLC example and find a counterexample. Although the probability of this logic error occurring is very small, it may cause the system to crash.
1. Einleitung
A PLC is an automatic control device that can receive logic input signals from sensors, computing devices, or other PLCs and output processed logic signals.
Control algorithms can be written using standard languages such as Ladder Diagram (LD), Structured Text (ST), or Instruction List (IL) [1].
PLCs use programmable language technology to control large-scale integrated circuits and have been widely used in industry [2]. Since safety-critical software can cause serious damage to life or property, verifying safety-critical software has become an indispensable step to ensure software quality. The current method of verifying PLCs still relies on simulation and testing. However, they do not cover all possible situations, especially whether the PLC’s design model meets the requirements. Therefore, model checking technology was introduced into the PLC field. Theoretical analysis and design of PLCs have become very important.
The first step in PLC model checking is to establish a PLC model, such as establishing a model from a functional diagram [3]. The PLC model focuses on establishing time attributes [4]. It can be modeled by the method of timed automata [5] or the time period modeling method [6]. Therefore, the state space of the model will be reduced compared to a timed automaton. No matter which method is chosen, an abstract model can finally be given [7]. How to establish a good PLC abstract model is the top priority of inspection. Manual modeling can easily introduce many errors, so it is very important to establish an integrated modeling and testing tool. This is one of the concerns of this article.
The PLC control program runs in a real-time operating system (multi-task or single-task); this article is mainly based on a multi-task scheduling PLC system. Section 2 introduces the modeling method of the PLC system. Section 3 gives the analysis and improvements of this model, as we need to reduce spurious errors. Section 4 designs a model checking tool, PLC-Checker, to check the established model, including introducing the method of converting a PLC program into SPIN input language, Promela code. Finally, a classic PLC example for checking and a critical computer example found by PLC-Checker.
2. PLC modeling*
This work was funded by NSFC 60973049, 60635020, and TNList interdisciplinary foundations. Model checking is divided into three steps: modeling, property description, and verification. The most important thing is how to build a system model. In the system, the PLC controller is not isolated but has interactions with the working environment, drivers, and people [8]. Therefore, these factors should also be modeled. The environment, people, and PLC controller are logically independent and parallel to each other. Furthermore, the input language of the model checker SPIN, Promela, is focused on describing concurrency, so starting from this idea, we build these factors into several concurrent processes to conform to SPIN’s checks, which will also accurately describe the system. For ease of description, they will be called concurrent entities. PLC controllers and concurrent entities are represented by symbols in the image table.
The symbols of the PLC system include I (input port), Q (output port), and M (middle relay). Figure 1 is a PLC system model diagram. Interval modeling strategy: Use bit states that mark which specific concurrent entity represents the concurrent entity in the state, regardless of the system clock. This may ignore differences in time states, thus simplifying the PLC model.
The modeling strategy does not add system clock attributes and does not completely correspond to the model of the original PLC. That is mainly because adding the system clock will cause the PLC system model to be too large, and there is no model checking tool to handle such a large model. The starting point for modeling the state is this, without taking into account the number of PLC scans when a transition has been experienced. No matter how many times you scan the experienced ones, they will all be included in this model. In other words, the real model will be a subset of the built model (time interval model). The real PLC environment is complex, including a
Various hardware and human behaviors are as follows
Wir werden verschiedene Arten von konkurrierenden Einheiten in der SPS-Umgebung analysieren.
1) Hardware-Einheit
The hardware entities of the PLC system are mainly some PLC-controlled equipment. The status of these devices can be used as input to the PLC controller. Therefore, the hardware entity is bound to its associated I and Q, and the hardware has its own workflow, which is determined by the hardware requirements. This workflow can be abstracted into an automaton. This automaton is used to describe the working status of the hardware. Definition 2.1. The hardware entity is a tuple Env =<ienv,qenv, a=””>, where Ienv is the I port entity bound to the hardware, and Qenv is the Q port bound to the entity. A is an automaton describing the workflow of an entity, and A is a tuple A =<s0, t=””>, where s0 is the initial state of A, S is the state set, and T is the transition set. The state of the hardware entity is a subset of the I symbol, and the IS symbol of each state is mapped to {True, False}. The state in which the I symbol does not appear can be true or false (i.e., act arbitrarily). The transfer of hardware entities is directly represented by a subset of Q symbols, indicating that all Q symbols in the subset will promote migration between countries at the same time. The state transition diagram of this hardware entity also needs to specify the initial state from which the transition diagram is drawn. </s0,></ienv,qenv,>
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. The human behavior entity is a tuple Env= <Ienv, A>, where Ienv is the I port, the hardware entity, and Qenv is the Q port bound to the entity. A is an automaton entity describing the workflow, and A is a tuple A =<s0, t=””>, where s0 is the initial state of A, S is the set of states, and T is the set of transitions. </s0,>
Human action entities are similar to hardware entities; they have the same state definition. It is difficult to simulate human behavior, especially when designing a PLC involves several individuals. In response to these difficulties, human behavior modeling should adopt an iterative process: first, a simple behavioral model is built using model validation; then, if no counterexample is found, for example, a more complex model is built and validated.
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
All transfers are genuine for verification. However, the verification of completely random behavior will lead to a sharp increase in the state space, so how to choose an appropriate human behavior model is a difficult point in modeling. If the human input is relatively simple, we can use completely random behavior modeling; otherwise, you need to seriously consider building a reasonable model of human behavior.
We model the behavior of the PLC environment and people, and then we model the PLC controller. The PLC controller will be in a cycle when rotating.
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.
The basic logic operation network of the PLC controller includes: S flip-flop, R flip-flop, SR flip-flop, EQ flip-flop, RS flip-flop, POS rising edge detector, NEG falling edge detector, etc. For basic logic operation network modeling, we adopt a direct mapping strategy, that is, the network behavior of the PLC controller model and the logical behavior of the network are completely equivalent. Where flip-flops, R flip-flop, SR flip-flop, EQ flip-flop, and RS flip-flop can be directly mapped to their behavior using Boolean expressions.
PLC Model Analysis and Improvement (Part 2)
