High reliability is key to the performance of electrical control equipment. PLC combines computer technology, automatic control technology and communication technology, and is widely used in the automation of industrial processes. Traditional verification methods cannot meet some requirements of complex PLC systems. In this paper an efficient PLC system modeling and verification method is proposed. In order to ensure the high-speed performance of PLC, we proposed the “time interval model” and “notification waiting” technology. It can reduce the state space and make it possible to verify some complex PLC systems. In addition, the conversion from the established PLC model to Promela language was obtained, and a tool PLC-Checker for PLC system modeling and checking was designed. Use PLC-Checker to check a classic PLC example and find a counterexample. Although the probability of this logic error occurring is very small, it may cause the system to crash.
1. Introduzione
Il PLC è un dispositivo di controllo automatico in grado di ricevere segnali di ingresso logici informativi da sensori, dispositivi informatici o altri PLC e di emettere segnali logici elaborati.
Gli algoritmi di controllo possono essere scritti utilizzando linguaggi standard come Ladder Diagram (LD), Structured Text (ST) o Instruction List (IL) [1].
Il PLC utilizza la tecnologia del linguaggio programmabile per controllare circuiti integrati su larga scala ed è stato ampiamente utilizzato nell'industria [2]. Poiché il software critico per la sicurezza può causare gravi danni alla vita o alle cose, la verifica del software critico per la sicurezza è diventata una fase indispensabile per garantire la qualità del software. L'attuale metodo di verifica del PLC si basa ancora sulla simulazione e sul test. Tuttavia, non coprono tutte le situazioni possibili, soprattutto se il modello di progettazione del PLC soddisfa i requisiti. Pertanto, la tecnologia di verifica del modello è stata introdotta nel campo dei PLC. L'analisi teorica e la progettazione dei PLC sono diventate molto importanti.
The first step in PLC model checking is to establish a PLC model, such as establishing a model from a functional diagram [3]. The PLC model focuses on establishing time attributes [4]. It can be modeled by the method of timed automata [5] or the time period modeling method [6]. Therefore the state space of the model will be reduced compared to a timed automaton. No matter which method is chosen, an abstract model can finally be given [7]. How to establish a good PLC abstract model is the top priority of inspection. Manual modeling can easily introduce many errors, so it is very important to establish an integrated modeling and testing tool. This is one of the concerns of this article.
Il programma di controllo PLC viene eseguito in un sistema operativo in tempo reale (multi-task o single-task); questo articolo si basa principalmente sul sistema PLC con programmazione multi-task. Sezione 2 L'articolo introduce il metodo di modellazione del sistema PLC. La sezione 3 fornisce l'analisi e i miglioramenti di questo modello, in quanto è necessario ridurre gli errori spuri. La sezione 4 progetta uno strumento di verifica del modello PLC-Checker per controllare il modello stabilito, introducendo anche il metodo di conversione del programma PLC in codice Promela del linguaggio di input SPIN. Infine, un classico esempio di PLC per la verifica e un esempio di computer critico trovato da PLC-Checker.
2.Modellazione PLC*
This work was funded by NSFC 60973049, 60635020 and TNList interdisciplinary foundations. Model checking is divided into three steps: modeling, property description and verification. The most important thing is how to build a system model. In the system, the PLC controller is not isolated, but has interactions with the working environment, drivers and people [8]. Therefore, these factors should also be modeled. The environment, people, and PLC controller are logically independent and parallel to each other. Furthermore, the input language of the model checker SPIN, Promela, is focused on describing concurrency, so starting from this idea, we build these factors into several concurrent processes to conform to SPIN’s checks, which will also accurately describe the system. For ease of description, they will be called concurrent entities. PLC controllers and concurrent entities are represented by symbols in the image table.
I simboli del sistema PLC includono I (porta di ingresso), Q (porta di uscita) e M (relè centrale). La Figura 1 rappresenta il diagramma del modello del sistema PLC. Strategia di modellazione a intervalli: Utilizzare stati di bit che segnano quale specifica entità concorrente rappresenta l'entità concorrente nello stato, indipendentemente dall'orologio del sistema. In questo modo si possono ignorare le differenze tra gli stati temporali, semplificando così il modello del PLC.
La strategia di modellazione non aggiunge gli attributi dell'orologio di sistema e non corrisponde completamente al modello del PLC originale. Ciò è dovuto principalmente al fatto che l'aggiunta dell'orologio di sistema rende il modello di sistema del PLC troppo grande e non esiste uno strumento di verifica del modello in grado di gestire un modello così grande. Il punto di partenza per la modellazione dello stato è questo, senza tenere conto del numero di scansioni del PLC quando si verifica una transizione. Indipendentemente dal numero di scansioni effettuate, quelle sperimentate saranno tutte incluse in questo modello. In altre parole, il modello reale sarà un sottoinsieme del modello costruito (modello a intervalli di tempo).L'ambiente PLC reale è complesso e comprende un
Vari hardware e comportamenti umani.
Analizzeremo diversi tipi di entità concorrenti nell'ambiente PLC.
1) Entità hardware
Le entità hardware del sistema PLC sono principalmente alcune apparecchiature controllate dal PLC. Lo stato di questi dispositivi può essere utilizzato come input per il controllore PLC. Pertanto, l'entità hardware è legata alle sue I e Q associate e l'hardware ha un proprio flusso di lavoro, determinato dai requisiti dell'hardware. Questo flusso di lavoro può essere astratto in un automa. Questo automa viene utilizzato per descrivere lo stato di funzionamento dell'hardware. Definizione 2.1. L'entità hardware è una tupla Env =
Il diagramma di transizione di stato dell'entità hardware si basa sulla divisione del simbolo I e l'attributo tempo non viene considerato. Il diagramma di transizione di stato dell'entità hardware è in realtà l'astrazione dell'entità hardware quando questa viene ignorata e la simulazione astratta richiede un riferimento all'hardware.
2) Un'entità di uscita semplice legata solo alla porta Q non utilizza la porta I, il che significa che l'entità di uscita semplice non ha un diagramma di transizione di stato. Un'entità di uscita semplice è un dispositivo che visualizza lo stato di funzionamento del PLC, come una luce. L'uso delle entità di uscita semplici è quello di legarsi alla porta Q in modo che il PLC possa progettare la propria logica.
3) Definizione delle entità comportamentali umane 2.2. L'entità comportamento umano è una tupla Env=
Le entità di azione umana sono simili alle entità hardware; hanno la stessa definizione di stato. È difficile simulare il comportamento umano, soprattutto quando la progettazione di un PLC coinvolge un certo numero di individui. In risposta a queste difficoltà, la modellazione del comportamento umano dovrebbe adottare un processo iterativo: prima si costruisce un modello comportamentale semplice utilizzando la convalida del modello; poi, se non si trova nessun contatore, ad esempio, si costruisce e si convalida un modello più complesso,
Fino a quando non viene trovato un controesempio o è difficile essere più complessi; infine, se non viene trovato alcun controesempio significativo, viene generato un modello di comportamento umano completamente casuale (cioè: il comportamento umano è un grafo completo).
Tutti i trasferimenti sono autentici) per la verifica. Tuttavia, la verifica di un comportamento completamente casuale porterà a un forte aumento dello spazio degli stati, quindi la scelta di un modello di comportamento umano appropriato è un punto difficile nella modellazione. Se l'input umano è relativamente semplice, è possibile utilizzare un modello di comportamento completamente casuale, altrimenti è necessario considerare seriamente la possibilità di costruire un modello ragionevole di comportamento umano.
Modelliamo il comportamento dell'ambiente e delle persone del PLC, quindi modelliamo il controllore del PLC. Il controllore del PLC sarà in ciclo quando ruota.
Il PLC legge tutti gli ingressi dalla porta I.
Il PLC calcola tutte le unità logiche.
PLC imposta tutte le porte Q.
L'unità di base del processo PLC è chiamata rete. Tutte le reti vengono eseguite in ordine numerico per l'impostazione in fase di progettazione.
La rete di funzionamento logico di base del controllore PLC comprende: flip-flop S, flip-flop R, flip-flop SR, flip-flop EQ, flip-flop RS, rilevatore del fronte di salita POS, rilevatore del fronte di discesa NEG, ecc. Per la modellazione della rete delle operazioni logiche di base, adottiamo una strategia di mappatura diretta, ovvero: il comportamento della rete del modello del controllore PLC e il comportamento logico della rete sono completamente equivalenti. Dove i flip-flop, i flip-flop R, i flip-flop SR, i flip-flop EQ e i flip-flop RS possono essere mappati direttamente al loro comportamento utilizzando espressioni booleane.