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 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. Introduction
PLC is an automatic control device that can receive information 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].
PLC uses programmable language technology to control large-scale integrated circuits and has 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 PLC 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 PLC has 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 multi-task scheduling PLC system. Section 2 The article introduces the modeling method of 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 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 behavior.the following
We will analyze different types of concurrent entities in the PLC environment.
1) Hardware entity
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 =
The state transition diagram of the hardware entity is based on the division of symbol I, and the time attribute is not considered. The hardware entity state transition diagram is actually the abstraction of the hardware entity when it is ignored, and the abstract simulation requires reference to the hardware.
2) A simple output entity that is only bound to the Q port does not use the I port, which means that the simple output entity does not have a state transition diagram. A simple output entity is a device that displays the working status of the PLC, just like a light. The use of simple output entities is to bind to the Q port so that the PLC can design its logic.
3) Definition of human behavioral entities 2.2. L'entità comportamento umano è una tupla Env=
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 a number of 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 counter is found, for example, a more complex model is built and validated,
Until a counterexample is found or it is difficult to be more complex; finally, if no meaningful counterexample is found before, a completely random human behavior model is generated (that is: human behavior is a complete 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.
Modelliamo il comportamento dell'ambiente e delle persone del PLC, quindi modelliamo il controllore del PLC. Il controllore del PLC sarà in ciclo quando ruota.
Il PLC legge tutti gli ingressi dalla porta I.
Il PLC calcola tutte le unità logiche.
PLC imposta tutte le porte Q.
L'unità di base del processo PLC è chiamata rete. Tutte le reti vengono eseguite in ordine numerico per l'impostazione in fase di progettazione.
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, RS flip-flop can be directly mapped to their behavior using Boolean expressions.
Italian 
English 
Russian 
German 
Spanish 
Portuguese 
French 
Dutch