11/12/2009

Analisi di modelli GRAFCET tramite generazione automatica dell’automa

temporizzato equivalente

Cristiano Poddie

Tesi di laurea specialistica inIngegneria Elettronica

Università degli Studi di Cagliari – DIEEENS Cachan - LURPA

Relatori:Prof. J.M. ROUSSEL

Prof. Alessandro Giua

Indice

2Analisi di modelli GRAFCET tramite generazione automatica dell’automa temporizzato equivalente

Analisi di modelli GRAFCET tramite generazione automatica dell’automa temporizzato equivalente Introduzione

• PLC, SFC e GRAFCET• Presentazione del problema• Differenze tra GRAFCET e automa temporizzato• Approccio utilizzato

Il grafo delle configurazioni stabili accessibili• Definizione• Configurazioni• Evoluzioni• Costruzione del GASC

- Albero delle configurazioni accessibili

Automa temporizzato• Costruzione• Analisi

Conclusioni

Introduzione

3Analisi di modelli GRAFCET tramite generazione automatica dell’automa temporizzato equivalente

PLC, SFC e GRAFCET

PLC• Controllore a logica

programmabile- Utilizzato nell’industria per il

controllo dei processi produttivi

SFC• Linguaggio di programmazione

- Linguaggio grafico, concetto di stato, causa, effetto, temporizzazioni

- Deriva dal linguaggio GRAFCET

GRAFCET• Linguaggio di modellazione

- Descrive il comportamento di un sistema

Introduzione

4Analisi di modelli GRAFCET tramite generazione automatica dell’automa temporizzato equivalente

Presentazione del problema Obiettivo

• Stabilire un metodo che consenta di descrivere il comportamento di un grafcet tramite un automa temporizzato equivalente

Motivazioni• GRAFCET

- linguaggio di modellazione molto completo e semplice da usare ma per il quale non sono disponibili molti strumenti di analisi

• Automa temporizzato- formalismo ampiamente studiato e per il quale sono disponibili diversi mezzi di

analisi

Approccio utilizzato• Modellazione realizzata tramite grafcet• Generazione automatica dell’automa temporizzato• Analisi dell’automa temporizzato ottenuto

Introduzione

5Analisi di modelli GRAFCET tramite generazione automatica dell’automa temporizzato equivalente

Grafcet• Più fasi attive simultaneamente• Scatto simultaneo di più transizioni• Approccio orientato alla condizione o

all’evento• Differenti forme e applicazioni delle

temporizzazioni

Differenze GRAFCET/automa temporizzato

Automa temporizzato• Solo uno stato attivo• Un solo evento per volta

• Approccio orientato solo agli eventi• Temporizzazioni: guardie, invarianti e

reset

Introduzione

6Analisi di modelli GRAFCET tramite generazione automatica dell’automa temporizzato equivalente

Approccio utilizzato:Passaggio per un modello intermedio

Perché un modello intermedio?• Per semplificare il meccanismo di costruzione

- Ricercare gli stati stabili raggiungibili e le evoluzioni del grafcet

- Rappresentare gli stati e le evoluzioni tramite l’automa temporizzato

Informazioni contenute nel modello intermedio• Informazioni necessarie all’analisi delle evoluzioni del grafcet

- Situazioni, uscite emesse successioni di scatti simultanei di transizioni

• Informazioni necessarie per l’automa temporizzato

- Eventi, guardie, invarianti e operazioni sugli orologi

Modello utilizzato• Estensione del grafo delle situazioni stabili accessibili

Grafo delle Configurazioni Stabili Accessibili

7Analisi di modelli GRAFCET tramite generazione automatica dell’automa temporizzato equivalente

Grafo delle Configurazioni Stabili Accessibili (GASC)

Composizione• Macchina mono-stato

- Stato: configurazione stabile del grafcet

- Evoluzione: passaggio da una configurazione stabile ad un’altra

- Tempo: livello logico

Configurazione del Grafcet• Situazione del grafcet

- Insieme di fasi attive• Stato delle temporizzazioni

- Insieme di temporizzazioni scadute

• Stato delle uscite- Insieme delle uscite attive

• Condizione di invarianza

Set di uscite attive

Set di temporizzazioni

scaduteSet di fasi attive

Condizione di invarianza

Grafo delle Configurazioni Stabili Accessibili

8Analisi di modelli GRAFCET tramite generazione automatica dell’automa temporizzato equivalente

GASC: Evoluzioni

Lista ordinata di insiemi di transizioni

Causa dell’evoluzione

Operazioni sugli orologi

Configurazione del grafcet• Situazione del grafcet• Stato delle temporizzazioni • Stato delle uscite

Evoluzioni tra le configurazioni• Condizione di evoluzione

- Condizione (o evento) che devono rispettare gli ingressi e le temporizzazioni

• Dettaglio dell’evoluzione- Lista ordinata degli insiemi di

transizioni che scattano• Operazioni sugli orologi

Grafo delle Configurazioni Stabili Accessibili

9Analisi di modelli GRAFCET tramite generazione automatica dell’automa temporizzato equivalente

Costruzione del GASC

Tecnica proposta• Costruire l’albero delle configurazioni

accessibili (TAC) per ogni configurazione stabile raggiungibile

- Radice: configurazione stabile da analizzare

- Nodo: configurazione raggiunta da analizzare

- Foglia: configurazione stabile raggiungibile

• Riportare sul GASC le evoluzioni stabili

- Tra radici e foglie

TAC

GASC

Albero delle configurazioni accessibili

10Analisi di modelli GRAFCET tramite generazione automatica dell’automa temporizzato equivalente

TAC: Radice

Informazioni date• Configurazione stabile da analizzare

Informazioni da calcolare• Transizioni che possono scattare • Insiemi di transizioni che possono

scattare simultaneamente (con la relativa condizione)- per ogni insieme un evoluzione

• Evoluzioni dovute al tempo

• Condizione di invarianza- Condizione booleana su ingressi

e temporizzazioni per cui la configurazione è stabile

Albero delle configurazioni accessibili

11Analisi di modelli GRAFCET tramite generazione automatica dell’automa temporizzato equivalente

TAC: nodo intermedio

Informazioni date• Configurazione raggiunta• Variazioni di ingressi e

temporizzazioni per cui è stata raggiunta la configurazione

Informazioni da calcolare• Transizioni che possono scattare• Insiemi di transizioni che possono

scattare

• Condizione di stabilità- Per le situazioni raggiunte

almeno parzialmente stabili Foglia

Automa temporizzato

12Analisi di modelli GRAFCET tramite generazione automatica dell’automa temporizzato equivalente

Automa temporizzato: costruzione

Stato• Per ogni configurazione stabile uno stato

dell’automa temporizzato

- Invariante ← Condizione di stabilità sulle temporizzazioni

Transizione• Per ogni evoluzione del GASC una

transizione dell’automa temporizzato

- Condizione di transizione ← condizione di evoluzione sugli ingressi

- Guardia:

• associare ad ogni espressione d/Xi una guardia xi ≥ d

• Associare ad ogni espressione d/Xi la guardia xi < d

- Associare, se necessario, dei reset per gli orologi

Automa temporizzato

13Analisi di modelli GRAFCET tramite generazione automatica dell’automa temporizzato equivalente

Analisi dell’automa

Studio della raggiungibilità• Verificare tramite software dedicato (per esempio UPPAAL) la

raggiungibilità degli stati dell’automa

• Verificare quali evoluzioni possono essere effettuate dall’automa

Automa temporizzato

14Analisi di modelli GRAFCET tramite generazione automatica dell’automa temporizzato equivalente

Semplificazione del GASC

• Se uno stato non è raggiungibile dall’automa eliminare la configurazione dal GASC

• Se un’evoluzione non può essere effettuata dall’automa eliminare il relativo arco dal GASC

• Condizione necessaria e sufficiente per la raggiungibilità

Conclusioni

15Analisi di modelli GRAFCET tramite generazione automatica dell’automa temporizzato equivalente

Conclusioni

Grafo delle Configurazioni Stabili Accessibili• Rappresentazione completa ma compatta

- Solo le configurazioni stabili sono riportate- Tutte le informazioni sulle possibili evoluzioni sono riportate

Risultati di questo lavoro• Un approccio per l’analisi di grafcet temporizzati

- Visione logica del tempo• Grafo delle Configurazioni Stabili Raggiungibili

- Visione fisica del tempo• Costruzione dell’automa temporizzato e analisi del grafo delle regioni

• Un algoritmo per ottenere automaticamente il GASC- Implementato su Python e attualmente in uso presso il laboratorio LURPA

• Probabile pubblicazione nel corso dell’anno 2010

INTRODUCTION 2/3

16Analisi di modelli GRAFCET tramite generazione automatica dell’automa temporizzato equivalente

Grazie per la vostra attenzione

Approfondimenti

17Analisi di modelli GRAFCET tramite generazione automatica dell’automa temporizzato equivalente

Esempio pratico (1)

Sistema di distribuzione acqua• Un serbatoio• 6 valvole• 2 pompe

Comportamento• Le pompe si alternano ogni 24 ore• Temporizzazioni nell’avvio pompe e

apertura valvole

Analisi• Le operazioni vengono eseguite

nell’ordine richiesto?• Esistono situazioni di pericolo?• Analisi manuale impossibile

Approfondimenti

18Analisi di modelli GRAFCET tramite generazione automatica dell’automa temporizzato equivalente

Esempio pratico (2)

Modello in GRAFCET• Analisi manuale impossibile

Risultati ottenuti con l’algoritmo utilizzato• 32 configurazioni raggiungibili• Nessuna instabilità• 670 evoluzioni possibili• Nessuna situazione di pericolo• Tempo impiegato: 15 secondi

circa su P4 2,4GHz

Approfondimenti

19Analisi di modelli GRAFCET tramite generazione automatica dell’automa temporizzato equivalente

TON sugli ingressi

1

2

1s/at1

F

T

atF

a ∙ 1sec/X1tTa

V

atV

tTb a

1s/a ← XV ∙ a + XT ∙ a ∙ 1sec/X1

Approfondimenti

20Analisi di modelli GRAFCET tramite generazione automatica dell’automa temporizzato equivalente

Non simultaneità tra eventi di ingresso ed eventi dovuti alle temporizzazioni

• p.d.f.: probability density function

• e: evento ‘variazione degli ingressi’

• 1s/Xi: temporizzazione sulla fase i

• hi: orologio associato alla fase i

p.d.f.(e)

1s/Xi

hi (sec)

t

t

tT(A) T(A+1)

1

Approfondimenti

21Analisi di modelli GRAFCET tramite generazione automatica dell’automa temporizzato equivalente

Esempio di utilizzo di UPPAAL (1)

Grafcet analizzato• specifiche:

- O2 deve essere emessa- O2 e O3 non devono mai

essere emesse simultaneamente

• Impossibile un’analisi manuale

Approfondimenti

22Analisi di modelli GRAFCET tramite generazione automatica dell’automa temporizzato equivalente

Esempio di utilizzo di UPPAAL (2)

Grafo delle configurazioni stabili raggiungibili

Approfondimenti

23Analisi di modelli GRAFCET tramite generazione automatica dell’automa temporizzato equivalente

Esempio di utilizzo di UPPAAL (3)

Automa temporizzato equivalente

Approfondimenti

24Analisi di modelli GRAFCET tramite generazione automatica dell’automa temporizzato equivalente

Esempio di utilizzo di UPPAAL (4)

Linguaggio UPPAAL• Implementazione di query

Query implementate• Raggiungibilità degli stati• Possibilità di evoluzione• Presenza di deadlock

Approfondimenti

25Analisi di modelli GRAFCET tramite generazione automatica dell’automa temporizzato equivalente

Esempio di utilizzo di UPPAAL (5)

GASC semplificato

Approfondimenti

26Analisi di modelli GRAFCET tramite generazione automatica dell’automa temporizzato equivalente

Esempio di GRAFCET con instabilità totale

Instabilità totale• Lo stesso insieme di transizioni scatta

due volte

Costruzione dell’albero delle configurazioni accessibili

• Nella costruzione individuiamo la seguente sequenza:

- <{t3}, {t2}, {t1}, {t2}>• L’instabilità totale viene riportata

all’analista insieme alla causa.

Approfondimenti

27Analisi di modelli GRAFCET tramite generazione automatica dell’automa temporizzato equivalente

Definizione formale del Grafo delle Configurazioni Stabili Accessibili