3. Analysis and improvement of PLC model
The previous section introduced the PLC modeling system. According to this strategy, we can abstract the PLC system into a formal model for model checking. Therefore, the credibility of this model will directly determine the model checking results. If the model does not completely cover the original system (we call it smaller than the original system), it may cause some errors to go undetected; if the real system can completely cover the model, but it contains many states that the original system does not have (we call it smaller than the original system) The original system is large), which may introduce some errors that do not exist in the real system. This is called a pseudo error. So there are two required modeling strategies.
First, in order to find all errors in the system, we should build a model large enough to cover all state original systems; second, the model is required to be as close to the real system as possible. This will not only reduce the state space, but also improve efficiency. Based on the requirements, we will analyze the time interval model. Proposition 1 If the time interval model conforms to the properties, the real PLC system model also conforms. The correctness of Proposition 1 can be concluded from the relationship between the two models. That means that everything that will happen to the real model is contained in the time interval model, the time interval model is larger than the real model. If you can’t find a counterexample by using the time interval model, you can prove the correctness of the real PLC model; on the other hand, if we find a counterexample, we can’t determine whether the real PLC system has errors. That is to say, the converse of Proposition 1 is false. Manual intervention is then required to analyze the counterexample to determine whether it is a spurious error.
The time interval modeling strategy can obtain a summary PLC model, and many studies based on NuSMV also use strategies similar to the time interval model to simulate PLC systems. However, the “time interval model” deviates greatly from the real model and needs to be improved. This deviation is: the “time interval model” does not reflect the characteristics of PLC’s high-speed scanning characteristics and low-speed scanning characteristics of concurrent entities. That is, all environmental changes should be scanned by the high-speed PLC, but the time interval model ignores the high-speed characteristics of the PLC, so changes in the external environment may not be scanned. In response to the above problems, taking into account the physical characteristics of external high-speed scanning and low-speed concurrency, the time interval modeling strategy will be improved by adding a notification waiting mechanism. Based on the interval model, each concurrent state entity must be blocked and wait somewhere after the transfer is completed.Only when the PLC controller has fully scanned at least once, the notification waiting mechanism will
The concurrent entity deletes the block and continues working. Then the transfer is completed. The process of the concurrent entity completing the migration through the notification waiting mechanism is shown in Figure 2:
t0: Transmission starts, blocks and notifies PLC controller.
t1-tm: PLC completely scans m times (m in
At least).
tm 1: The concurrent entity receives the notification PLC and the transfer is completed.
This mechanism ensures that each state change of a concurrent entity can be scanned by the PLC controller at least once. Proposition 2 After adding the notification waiting mechanism, the model becomes a subset of the time interval model.exist
At the same time, the model can also include all situations in the real model. In other words, if a model adds a notification waiting mechanism that conforms to the attributes, the real PLC system model also conforms. Using Proposition 1 to prove Proposition 2 is similar. Through Proposition 2, we can see that the mechanism model still has good properties after adding notification waiting. As mentioned before, abstract system models have two requirements: first, that the real system be completely included, and second, that the model be as close as possible to the real system. The first proposition is to prove that the time interval model includes the real system. As long as model checking tools are used to prove that the abstract model satisfies certain properties, then the real properties of the system will also satisfy this. But this model is not exactly equal to the real model, it should be much larger than the real model. Compared with time interval models, this model further reduces the distance between real systems, greatly reducing the chance of detecting spurious errors.
A model checking tool will give a counterexample that violates the system’s property; it is easy to determine manually whether a counterexample in a real system is true or not. If the error in the original system really exists, then we find a counterexample. Otherwise, the error is because the abstract model is larger than the real system, which is a spurious error. Therefore, although this time interval model is not completely equivalent to the original system, through this model we can judge whether a system satisfies a certain property, and if not we can find a specific counterexample (more checks are still needed to determine whether it is a pseudo error). The model is not equivalent to the original system mainly because there are many factors that are difficult to model in the actual system, some of which may lead to errors. If all factors were modeled, this would result in building a huge model that cannot be checked, or simply cannot be implemented. The time interval model abstracts key factors from the real system and models them, greatly reducing the state space and reducing time complexity. At the same time, through the notification waiting mechanism, the model becomes closer to the real system, which not only reduces the time complexity, but also reduces the pseudo errors mentioned earlier.
NuSMV) check is implemented on the model established above. 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.spinroot.com. We will introduce the three parts of the PROMELA 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 assign the value of the output port through logic
Count all input ports.This is the translation
PLC network method.