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.
Se nel sistema PLC sono presenti errori difficili da individuare, essi sono dovuti principalmente a errori di progettazione logica, ma non a errori di calcolo.
Descrizione della logica dei bit. Pertanto, per semplificare il modello del programma PLC e concentrarsi sulla verifica del modello, si adottano 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 l'ispezione utilizziamo lo strumento di verifica dei modelli SPIN (il nostro PLC-Checker implementa anche NuSMV sul modello stabilito in precedenza). 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 i due linguaggi sono semanticamente simili, quindi forniamo alcuni esempi
Mostra 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 di 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.
Ecco un esempio di conversione di una rete SR:
if ::Exp(R) == 1 -> Q = 0; ::else -> if ::Exp(S) == 1 -> Q = 1; ::else -> skip; fi; fi; /* Exp(S) è l'espressione booleana della porta S Exp(R) è l'espressione booleana della 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ì:
atomico { if :: Q1 -> {IB, goto StateB} :: Q2 -> {IC, goto StateC} fi;} /* StateA è l'etichetta dello stato A Q1, Q2 è la condizione di trasferimento IB è impostare il valore dello stato sul valore dello stato B goto StateB significa saltare allo stato B */
3) Codice della proprietà
Le proprietà sono regole 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 dobbiamo usare la macro ing. Per prima cosa dobbiamo definire tutte le proposizioni in macro in LTL (come #define p i5 == 0), poi usiamo le proposizioni definite per formare formule 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 si chiama 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 per verificare 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. Aiuta a costruire modelli visivi e a eseguire ispezioni, e può fornire una semplice analisi dei risultati. Naturalmente, il controesempio che trova 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 nel verificare il modello di canale a due porte nel modo seguente. Per isolare la stanza dal mondo esterno si utilizzano due porte di passaggio.
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ò vedere, 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 è ancora molto imperfetto, come ad esempio la sua elaborazione come timer. Ma presenta grandi e unici vantaggi per la risoluzione dei problemi di esplorazione degli stati. Stiamo ancora esplorando attivamente questi problemi.
Italian 
English 
Russian 
German 
Spanish 
Portuguese 
French 
Dutch