3) Human behavioral entities
Definition 2.2. The human behavior entity is a tuple Env=
Human behavioral entities are similar to hardware entities;
They have the same status 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 example is found, a more complex model is built and verified until a counterexample is found or more difficult to find. Complex; finally, if no meaningful counterexample is found before, a completely random human behavior model is generated (ie: human behavior is a complete graph and all transfers are true) 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.
The PLC reads all inputs from the I port.
PLC calculates all logic units.
PLC sets all Q ports.
The basic unit on the PLC process is called a network. All networks will run in numbered order for design-time setup.
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. To model the basic logic operation network, we adopt a direct mapping strategy, that is, the controller model of the PLC network behavior is completely equivalent to the logical behavior of the network. 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.
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 countercase 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 model 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 environment changes should be scanned
High-speed PLC, but the time interval model ignores the high-speed characteristics of PLC, so changes in the external environment may not be scanned.In response to the above problems, considering external high-speed scanning and low-speed concurrency
Physical properties and time interval modeling strategies 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 scanned completely at least once, the notification waiting mechanism will send a message to the concurrent entity to remove the block and continue working. Then the transfer is completed. The process of migration of concurrent entities through the no-time waiting mechanism is shown in Figure 2:
This mechanism ensures that the PLC controller scans each state change of concurrent entities at least once. Proposition 2 After adding the notification waiting mechanism, the model becomes a subset of the time interval model. 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 so 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 lead to building a huge model that is impossible to check, or simply impossible to implement. 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.