PLC System Modeling Approach (Part 1)
PLC Model Analysis and Improvement (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, to simplify the PLC program model and focus on model checking, we
Effettuare le seguenti impostazioni:
Il PLC è un programma di controllo logico e tutte le variabili di controllo hanno solo due stati: 0 e 1;
I programmi PLC vengono eseguiti in un ambiente concorrente. In questo caso, è più probabile che la programmazione del PLC presenti errori non facili da individuare.
Alla luce di queste caratteristiche, per la verifica utilizziamo lo strumento di model checking SPIN (il nostro strumento PLC-Checker implementa anche NuSMV). Abbiamo formulato una serie di regole di conversione per costruire il modello di cui sopra nel linguaggio di input Promela di SPIN. Anche gli attributi del sistema devono essere tradotti in Promela. SPIN li mette insieme e poi esegue il rilevamento.
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 PRO MELA 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. Tutte le porte di ingresso vengono calcolate assegnando logicamente i valori delle porte di uscita. Ecco come tradurre una rete PLC.
Ecco un esempio di conversione di una rete SR:
se
::Exp(R) == 1 -> Q = 0;
::Others->
if::Exp(S) == 1 -> Q = 1;
::else -> skip; pheasant;
Fei;
/* Exp(S) è l'espressione booleana della porta S
Exp(R) è un'espressione booleana per la porta R
Q è la porta di uscita*/
2) Codice degli enti concorrenti
Riteniamo che ogni entità concorrente sia un processo unico, indipendentemente dal comportamento umano o dalle apparecchiature. Questi processi condividono le variabili con il processo di controllo del PLC. Questo deve essere fatto per garantire la concomitanza del sistema. Nella seconda parte di questo articolo, abbiamo discusso che tutte le entità concorrenti sono modellate come automi. Questo automa significa passare da uno stato all'altro. Utilizziamo le porte I per formare lo stato dell'entità. Utilizziamo le istruzioni goto come salti (proprio come nel linguaggio assembly). Un semplice esempio si presenta così:
Stato A:
atomo{
se
:: Q1 -> {IB, goto StateB}
:: Q2 -> {IC, goto StateC}
Filippine;}
/* StatoA è l'etichetta dello stato A
Q1 e Q2 sono condizioni di trasferimento
IB è impostare il valore dello stato sul valore dello stato B
goto StateB means jump to state B */
3) The property code is a rule that the PLC system must comply with. We use an LTL (Linear Time Logic) formula as input format. We should write the opposite property because of the mechanism of SPIN. SPIN will find that 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 una macro in LTL (come #define p i5 == 0), si utilizza la proposizione definita per formare la formula LTL. Spin può convertire automaticamente le formule LTL in codici PRO MELA utilizzando il comando “SPIN-f” (per maggiori dettagli, consultare il manuale SPIN).
4) Meccanismo di attesa delle notifiche
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.spinroot.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 for 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. Eseguire PLC-Checker
Dimostreremo l'efficacia del controllore PLC nella verifica del modello di canale a due porte nel modo seguente. Un passaggio a due porte viene utilizzato per isolare la stanza dal mondo esterno. Inserendo nello strumento il diagramma ladder e le entità concorrenti, che rappresentano la definizione delle proprietà, si esegue una verifica. La Figura 3 mostra i risultati. Come si può notare, c'è un errore nel risultato. Questo è dimostrato dalla verifica degli indizi che sono un vero controesempio all'archiviazione manuale. In altre parole, il nostro meccanismo è efficace nella verifica di tali programmi PLC.
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 establishes a concurrent entity model through a 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 of timers. But it has great and unique advantages for solving state exploration problems. We are still actively exploring such issues.
