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

3. Analisi e miglioramento del modello PLC

La sezione precedente ha introdotto il sistema di modellazione del PLC. Secondo questa strategia, possiamo astrarre il sistema PLC in un modello formale per la verifica del modello. Pertanto, la credibilità di questo modello determinerà direttamente i risultati del model checking. Se il modello non copre completamente il sistema originale (lo chiamiamo più piccolo del sistema originale), può far sì che alcuni errori non vengano rilevati; se il sistema reale può coprire completamente il modello, ma contiene molti stati che il sistema originale non ha (lo chiamiamo più piccolo del sistema originale), il sistema originale è grande), il che può introdurre alcuni errori che non esistono nel sistema reale. Questo è chiamato pseudo-errore. Quindi ci sono due strategie di modellazione necessarie.

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) Codice del controllore PLC

Un controllore PLC è costituito da più reti.

Anche il codice per il controllore PLC viene generato dalla rete. Naturalmente, prima di fare ciò, è necessario dichiarare le variabili necessarie. Ogni rete ha le sue porte di ingresso e di uscita, e ogni porta può essere rappresentata da un'espressione booleana. Assegniamo il valore della porta di uscita attraverso la logica

Conta tutte le porte di ingresso.

Metodo di rete PLC.