Università di Firenze – Dipartimento di Sistemi e Informatica
Attività dell’Unità di Firenze attinenti a
modellazione, simulazione e analisi
di sistemi reattivi distribuiti nello spazio
G.Bucci, E.Vicario, F.Baldini, L.Sassoli
{bucci,vicario,fbaldini, sassoli}@dsi.unifi.it
Sistemi reattivi tempo dipendenti
•
La correttezza dipende requisiti non funzionali
 Tempificazione degli eventi
 Sequenzializzazione degli eventi
 Applicazioni di controllo industriale, Componenti di software
embedded, …
•
In molti contesti diventano rilevanti anche aspetti legati alla
spazialità
 Configurazione spaziale del sistema
 Vincoli di tipo spaziale
 Evoluzione dinamica del sistema
Esempio:
Sistemi di instradamento del traffico ferroviario
•
•
•
Regolazione degli scambi
Regolazione dei semafori
Distanziamento
Esempio:
Celle di assemblaggio AGV (Automatic Guided Vehicles)
•
•
•
Rispetto della sequenza e dei tempi delle lavorazioni
Collision avoidance: modellazione di sensori ed
elaborazione di dati da essi provenienti
Deadlock avoidance: controllo dell’instradamento per
evitare la congestione
Esempio:
Reti ad hoc
•
Sistemi di esplorazione con controllo remoto
 Controllo della distanza reciproca delle unità per il
mantenimento della connessione wireless col sistema di
controllo
Modellazione con Reti di Petri Tempificate
•
Time Petri Nets permettono la
specifica e la validazione di:
 Tempificazione
 Sequenzializzazione
•
E.g. sistemi di controllo industriale:
 Ogni lavorazione richiede un tempo

•
minimo (e massimo) per il completamento
Le lavorazioni devono essere svolte
secondo una sequenza
(e.g. catena di montaggio)
Problema: i modelli TPN non permettono di catturare le
caratteristiche spaziali del sistema
 Evoluzione della configurazione spaziale nel tempo (mobilità)
 Vincoli di spazialità legati alla configurazione dell’ambiente e alla
evoluzione dinamica
Visualizzazione in un ambiente virtuale della evoluzione
spaziale controllata da un modello TPN
•
•
La presenza di un gettone in un
posto indica uno stato di
operazione per un oggetto mobile
Il progresso di una transizione
modella la condizione di
esecuzione di una azione nello
spazio
(e.g. spostamento lungo un
percorso predefinito)
Esempio:
applicazione al controllo di instradamento del traffico
•
In fase di simulazione il modello TPN simula il software di
controllo del sistema
 Genera comandi per le unità mobili in accordo alla tempificazione e

alla sequenzializzazione espressa nel modello
Permette la visualizzazione della evoluzione dello stato del controllo
(Token Game) e della configurazione spaziale del sistema
(Animazione)
[5,5]
Muovi_treno1
-> stazione
[3,3]
Treno1_prosegui ->
prossima stazione
Stazione
[2,2]
[5,5]
Muovi_treno2
Muovi_treno2
Limiti nella modellazione
•
•
L’evoluzione del modello TPN non è condizionata dalla
configurazione spaziale e dalla velocità degli oggetti mobili
Esempio: cella di assemblaggio con due veicoli AGV
 I veicoli si muovono sul percorso assegnato per il tempo determinato

dalla transizione
Le collisioni tra veicoli non sono rilevate né gestite
[100,100]
[98,98]
[99,99]
Move Truck1
Truck1
[100,100]
[98,98]
[99,99]
Move Truck2
Limiti nella modellazione
•
La configurazione spaziale deve potere condizionare la evoluzione
dello stato logico
 La configurazione spaziale è parte dello stato del modello
 L’occorrenza di una condizione nella configurazione spaziale
costituisce un evento che modifica lo stato logico
[100,100]
[98,98]
[99,99]
Move Truck1
Truck1
[98,98]
[99,99]
[100,100]
Move Truck2
Estensione del modello TPN
•
Il modello deve includere informazioni spaziali e cinematiche
 Posizione degli oggetti mobili
 Percorso su cui sono instradati
 Velocità degli oggetti mobili
•
L’evoluzione del modello deve accoppiare l’evoluzione delle
componenti logica e spaziale dello stato
 Leggi cinematiche che aggiornano la posizione degli oggetti mobili in
base al progresso nell’esecuzione delle transizioni
 Condizionamento della evoluzione dello stato logico del modello alla
configurazione spaziale del sistema
Spatial TPN
oggetti, percorsi, velocità
•
•
Ogni transizione del modello può essere associata a un oggetto
mobile, un percorso su cui l’oggetto è instradato, e un valore di
velocità
La transizione opera come controllore per l’oggetto
 L’oggetto è instradato sul path associato
 L’oggetto si muove con il valore di velocità associato alla transizione
y
[100,100]
y2
Move Truck1, Path p1, Speed 10
Truck1
y1
Position
(x1,y1)
Path p1
[100,100]
Move Truck2, Path p2, Speed 10
Path p2
x1
x2
x
Spatial TPN:
Aggiornamento della configurazione spaziale
•
•
•
Aggiornamento della posizione degli oggetti mobili
Cambiamento del percorso di instradamento
Variazione della velocità
y
[98,98]
[99,99]
[100,100]
Move Truck1
Truck1: (x1+speed*2T,y1)
(x1,y1)
(x1+speed*T,y1)
T
y1
T
[100,100]
Path p1
Truck1
Move Truck2
Truck2: (x2,y2)
Path p2
x1
x1+speed*T
x1+speed*2T
x
Spatial TPN:
Guardie sulla configurazione spaziale
•
L’evoluzione dello stato logico del modello è condizionata dalla
configurazione spaziale attraverso vincoli sulla posizione relativa
degli oggetti mobili
 condizioni relative alla presenza di una unità mobile su un path e/o
entro una distanza
[100,100]
Move AGV1
Truck1:(x1,y1); Path p1; Speed 10
[100,100]
Truck1
Move AGV2
Sensing
Field
Truck1:(x1,y1); Path p1; Speed 10
Vincoli: forward sensing system
Modellazione, simulazione e analisi
nell’ambiente ORIS
Time Petri Nets
TPN Editor
TPN Animator
TPN Analyzer
3D Objects
3D Object
Assembler
3D Environments
3D Environment
Composer
3D Environment
Animator
Tool di modellazione
•
Editor TPN
 Interfaccia grafica per la creazione di modelli di Petri
 Permette la specifica di intervalli temporali per le transizioni
•
e la specifica delle condizioni iniziali
Estensione al caso di sistemi con caratteristiche spaziali
 Oggetti mobili
 Percorsi
 Caratteristiche cinematiche (velocità)
Tool di modellazione
•
3D Object Assembler
 Assemblaggio di oggetti virtuali 3D da librerie di componenti
 Implementazione basata su Java 3D
•
Attualmente il tool permette la modellazione di robot virtuali
 È possibile creare librerie per la creazione di oggetti 3D diversi
Tool di modellazione
•
Virtual Environments Composer
 Organizza su una scena gli oggetti creati con 3D Object Assembler
 Definizione dei percorsi e dei parametri specifici per gli oggetti
mobili
•
Possibile estensione del tool per la creazione di schemi di
visualizzazione diversi
(e.g. visualizzazione 2D di un quadro sinottico ferroviario)
Tool di Simulazione
• TPN Animator (Token game
tempificato)
 Mostra l’evoluzione del modello
TPN nel tempo
 Produce i comandi di animazione
per gli oggetti mobili
•
3D Environment Animator
 Ricostruisce gli ambienti virtuali
creati con il tool “Environment
Composer”
 Riceve i comandi da TPN
Animator e gestisce l’esecuzione
dei thread di animazione
Esempio:
simulazione di un sistema di instradamento ferroviario
•
[7,7]
Il modulo di presentazione può
essere adattato a contesti
applicativi diversi e a simulatori
diversi (2D e 3D)
T1 prosegui – b1
Vincolo: b1 libero
[5,5]
[5,5]
T1 prosegui – b2
Vincolo: b2 libero
T1 move-scambio, speed=2
[5,5]
Stazione
[5,5]
T2 move-stazione, speed=5 T2 prosegui, speed=5
Binario b1
Treno T2
Binario b2
Treno T1
Analisi dello spazio degli stati
•
•
•
Lo stato di un modello TPN dipende da:
 Marcamento
 Insieme dei time to fire delle transizioni in progresso
Nei modelli TPN estesi per la modellazione di sistemi con spazialità,
questo include anche lo stato degli oggetti mobili
 Posizione degli oggetti
 Percorso su cui attualmente sono instradati
Enumerazione dello spazio degli stati
 Grafo di raggiungibilità
 Informazioni sui comportamenti critici rispetto a vincoli di tempo reale o di

configurazione spaziale
Calcolo della probabilità degli stati
Esempio
cella di assemblaggio con automatic guided vehicles (AGV)
• Gestione del traffico
 Assenza di collisioni basato su “controllo in avanti”

(forward sensing control) sui veicoli mobili
Assenza di stalli
• Il comportamento del sistema
Unload Area
AGV2
Unload
Area AGV1
è difficilmente predicibile
 Il controllo è complesso
 Le tempificazioni delle

operazioni di manipolazione e degli
istanti di partenza dei
veicoli sono non deterministiche
Dipendenza da vincoli spaziali
Load Area
AGV1
Load Area
AGV2
AGV2
AGV1
Docking
Station
Modellazione con il tool ORIS
•
•
TPN Editor: modello di Petri
Virtual Environments Composer: arrangiamento iniziale e
traiettorie
ANALIZZATORE
Rilevazione di stalli
(situazioni in cui i veicoli non
possono procedere senza collidere)
Risultati sperimentali preliminari nell’analisi
• La simulazione dà solo parziale confidenza sul corretto funzionamento
del sistema e sulla assenza di stalli
• L’analisi esaustiva dello spazio degli stati del modello TPN esteso
permette di avere garanzie di correttezza:
 Rilevazione delle situazioni di stallo
 Identificazione degli sfasamenti critici tra gli istanti di partenza dei veicoli
0
Ritardo partenza di AGV1
risp. a
AGV2 di AGV1
Partenza
Numero di stati
generati
Numero di deadlock
rilevati
Sfasamenti
AGV1 [0,40]
AGV2 [0,0]
Partenza
434939
32
AGV1 [0,0]
AGV2 [0,40]
319695
Istante di partenza
di
AGV2
0
critici
40 sec
Ritardo partenza di AGV2
19
risp. a AGV1
istanti critici
40 sec
40 sec