4. Controllo del modello di PLC
Il PLC è ampiamente utilizzato in molte applicazioni e dispone di numerosi dispositivi; rappresenta un'ampia area di ricerca. Il lavoro del PLC coinvolge diverse apparecchiature e persone, quindi il sistema PLC è concorrente. Allo stesso tempo, se ci sono errori in un sistema PLC, è difficile trovarli, soprattutto a causa di errori di progettazione logica, ma non di calcolo. Pertanto, ci concentriamo sul processo logico del programma di rilevamento del PLC e questa logica può essere descritta completamente dalla logica dei bit.
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.
Il linguaggio PROMELA è un linguaggio simile al C e sono semanticamente simili. Pertanto, ci limitiamo a fornire alcuni esempi per mostrare i concetti di base della traduzione. Per informazioni dettagliate sul linguaggio PROMELA, visitare il sito www.spin root.com. Introdurremo le tre parti del file PRO MELA come input a 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;
::Altri->
if::Exp(S) == 1 -> Q = 1;
::else -> salta; fagiano;
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 significa saltare allo stato B */
3) Il codice propertyProperty è una regola che il sistema PLC deve rispettare. Utilizziamo la formula LTL (Linear Time Logic) come formato di input. Dovremmo scrivere la proprietà opposta a causa del meccanismo di SPIN. SPIN troverà il nostro caso di proprietà, che dovrebbe essere un controesempio. Non possiamo scrivere direttamente la formula LTL, ma utilizziamo la macro ing. Innanzitutto dobbiamo definire tutte le proposizioni
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
Nella discussione sulla modellazione, si raccomanda di non aggiungere un meccanismo di attesa temporale. Questo meccanismo deve essere riflesso anche nel codice. L'implementazione specifica consiste nel firmare una variabile bit di ogni processo non PLC (ad eccezione di tutti i controllori PLC di processo) come segnale. Quando l'automa passa a un'etichetta di stato, la variabile segnale viene impostata su 0 e l'assegnazione successiva richiede che questa variabile sia 1 per continuare. Questo processo continua grazie alle caratteristiche della sintassi di PROMELA. Nel processo PLC non c'è questa restrizione. Al contrario, il processo PLC può impostare queste variabili a 1, garantendo così che ogni fase venga completata attraverso almeno una scansione del PLC. Questo meccanismo è chiamato meccanismo di attesa della notifica. Seguendo i quattro passaggi sopra descritti, otteniamo un file di input SPIN completo per il nostro sistema. Possiamo quindi utilizzare SPIN
Controllare il modello. Per un controllo passo-passo del modello SPIN, consultare il manuale SPIN (visitare www.spin root.com). SPIN fornirà il risultato se è stato trovato un controesempio. Possiamo usare la teoria per analizzare il file di tracciamento fornito da spin di cui sopra.
Utilizzando questo meccanismo di rilevamento, abbiamo sviluppato uno strumento di controllo del modello PLC-checker. Esso facilita la creazione di modelli visivi e di implementazioni di ispezioni e consente una semplice analisi dei risultati. Naturalmente, il controesempio trovato deve essere controllato manualmente per determinare se si tratta di un vero controesempio. Tuttavia, con l'aiuto dei file di traccia, questo non è un compito molto difficile. Abbiamo anche utilizzato con successo alcuni verificatori PLC (illustrati nella prossima sezione). Nell'esempio classico del libro di testo, è stato trovato un controesempio. Sebbene la probabilità di controesempi sia molto bassa, essi si verificano e possono avere gravi conseguenze. Questo strumento dimostra anche la correttezza e la validità della teoria di questo articolo.
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 conclusione
In questo lavoro studiamo la teoria della modellazione e del controllo del PLC utilizzando metodi formali. I requisiti analizzano le caratteristiche della modellazione del PLC e stabiliscono un modello di entità concorrente attraverso la strategia dell'intervallo di tempo. Dimostriamo poi che il modello a intervalli di tempo è un superset di sistemi PLC e riduciamo il modello aggiungendo un meccanismo di attesa senza tempo. Questo modello garantisce inoltre che tutte le modifiche al sistema possano essere analizzate dal controllore del PLC. Abbiamo scoperto che è possibile trovare errori in un sistema esaminando i suoi controesempi. Infine, viene illustrato l'uso di SPIN per verificare il modello. È presente anche una corrispondente introduzione allo strumento di verifica del modello PLC-Checker. In questa fase, il meccanismo presenta ancora molte imperfezioni, come la sua gestione come timer. Ma presenta grandi e unici vantaggi per la risoluzione di problemi di esplorazione degli stati. Stiamo ancora esplorando attivamente questi problemi.
