Form-based PLC modeling and verification method (Part 2)

4. PLC model checking

PLC is widely used in many applications and has many devices; it is a large area of ​​research. Any PLC work involves different equipment and people, so the PLC system is concurrent. At the same time, if there are some errors in a PLC system, it is difficult to find them, mainly because of logical design errors, but not calculation errors. Therefore, we focus on the PLC detection program logic process, and this logic can be completely described by bit logic.Therefore, in order to simplify the PLC program model and focus on model checking, we

Make the following settings:

 PLC is a logic control program, and all control variables have only two states: 0 and 1;

 PLC programs run in a concurrent environment. In this case, the PLC programming is more likely to have some errors that are not easy to find.

In view of the above characteristics, we use the model checking tool SPIN (our tool PLC-Checker also implements NuSMV) to check. We formulated a series of conversion rules to build the above model into SPIN’s input language Promela. System attributes also need to be translated into Promela. SPIN puts them together and then performs detection.

The PROMELA language is a C-like language and they are semantically similar. So we just give some examples to show the basic concepts of translation. To view detailed information about the PROMELA language, visit www.spin root.com. We will introduce the three parts of the PRO MELA file as input to SPIN.

1) PLC controller code

A PLC controller consists of multiple networks.

The code for the PLC controller is also generated from the network. Of course, before doing this, you should declare the variables you need. Each network has its input and output ports, and each port can be represented by a Boolean expression. We calculate all input ports by logically assigning the values ​​of the output ports. This is how to translate a PLC network.

Here is an example of converting an SR network:

if

::Exp(R) == 1 -> Q = 0;

::Others->

if::Exp(S) == 1 -> Q = 1;

::else -> skip; pheasant;

Fei;

/* Exp(S) is the Boolean expression of the S port

Exp(R) is a Boolean expression for the R port

Q is the output port*/

2) Code of concurrent entities

We believe that each concurrent entity is a unique process, regardless of human behavior or equipment. These processes share variables with the PLC controller process. This must be done to ensure system concurrency. In the second part of this article, we discussed that all concurrent entities are modeled as automata. This automaton means to move from one state to another. We use I ports to form the entity’s state. Use goto statements as jumps (just like in assembly language). A simple example looks like this:

Status A:

atom{

if

:: Q1 -> {IB, goto StateB}

:: Q2 -> {IC, goto StateC}

Philippines;}

/* StateA is the label of state A

Q1 and Q2 are transfer conditions

IB is to set the state value to the value of state B

goto StateB means jump to stateB */

3) The propertyProperty code is a rule that the PLC system must comply with. We use LTL (Linear Time Logic) formula as input format. We should write the opposite property because of the mechanism of SPIN. SPIN will find our case property happens, that should be a counterexample. We cannot write the LTL formula directly, but use the ing macro.First we should define all propositions

In a macro in LTL (such as #define p i5 == 0), then we use the defined proposition to form the LTL formula. Spin can automatically convert LTL formulas into PRO MELA codes using the “SPIN-f” command (see more details in the SPIN manual).

4) Notification waiting mechanism

In the modeling discussion, we recommend not adding a time wait mechanism. This mechanism also needs to be reflected in the code. The specific implementation is to sign a bit variable of each non-PLC process (except all process PLC controllers) as a signal. When the automaton transitions to a state label, the signal variable is set to 0, and the next assignment requires this variable to be 1 to continue. This process continues due to PROMELA syntax features. There is no such restriction in the PLC process. Instead, the PLC process can set these variables to 1, thereby ensuring that each step must be completed through at least one PLC scan. This is called a notification waiting mechanism. Following the four steps above; we get a complete SPIN input file for our system. Then we can use SPIN

Check the model. For a step-by-step checker of the SPIN model, see the SPIN manual (visit www.spin root.com). SPIN will give the result of whether a counterexample is found. We can use theory to analyze the tracking file given by spin mentioned above.

Using this detection mechanism, we developed a tool model checking PLC-checker. It facilitates the establishment of visual models and implementations of inspections, and allows for simple analysis of the results. Of course, the counterexample it finds should be checked manually to determine whether it is a true counterexample. However, with the help of trail files, this is not a very difficult task. We also successfully used some PLC checkers (shown in the next section). In the classic textbook example, a counterexample was found. Although the probability of counterexamples is very low, they do occur and can have serious consequences. This tool also proves the correctness and validity of the theory of this article.

5. Run PLC-Checker

We will demonstrate the effectiveness of the PLC checker in checking the two-gate channel model in the following way. A two-door passage is used to seal off the room from the outside world. By entering the ladder diagram and concurrent entities into the tool, which is the definition of the properties, we perform a check. Figure 3 shows the results. As we can see, there is an error in the result. This is proven by checking the clues to be a real counterexample to manual archiving. That is to say, our mechanism is effective in checking such PLC programs.

6.in conclusion

We study the modeling and checking theory of PLC using formal methods in this paper. The requirements analyze the characteristics of PLC modeling and establish a concurrent entity model through time interval strategy. We then prove that the time interval model is a superset of PLC systems and reduce the model by adding a time-free waiting mechanism. It also ensures that all changes to the system can be scanned by the PLC controller. We discovered that we can find errors in a system by examining its counterexamples. Finally, the use of SPIN to check the model is given. There is also a corresponding introduction to the model checking tool PLC-Checker. At this stage, the mechanism still has many imperfections, such as its handling as a timer. But it has great and unique advantages for solving state exploration problems. We are still actively exploring such issues.