Cristiano Poddie è nato a Sorgono (NU - Italia) il 16 Febbraio 1984. Ha conseguito la Laurea Specialistica in Ingegneria Elettronica nel 2009 presso il Dipartimento di Ingegneria Elettrica ed Elettronica dell'Università degli Studi di Cagliari. Ha sviluppato la sua tesi di laurea specialistica presso il laboratorio universitario di ricerca in produzione automatizzata LURPA dell'Ecole Normale Superieure de Cachan (Parigi - Francia) grazie a una borsa di studio internazionale messa a disposizione dalla stessa Ecole Normale Superieure di Cachan
Cristiano Poddie was born on February 16th 1984 in Sorgono (Italy). He obtained the Laurea Specialistica (Master) in Electronic Engineering in the 2009 at the Department of Electrical and Electronic Engineering, University of Cagliari. His thesis research work was done within the LURPA laboratory (Ecole Normale Superieure de Cachan) and it was supported by an ENS international scholarship.
Relatori/Advisors
Prof. Jean-Marc Roussel (LURPA - ENS Cachan)
Prof. Alessandro Giua (DIEE - UNICA)
Risorse/Resources
Tesi/Thesis [.pdf]
Slides [.ppt]
Analysis of grafcet models by automatic generation of the equivalent timed automaton
Abstract
The objective of this thesis is to give a contribution to solving the problem of formal verification on GRAFCET models with time requirements. GRAFCET is a standardized graphical model used to describe the behavior of sequential logic systems. Currently, all solutions offered to engineers to perform formal verification on GRAFCET models are based on simulation techniques. However, the generation of simulation sequences is an error-prone, tedious and time-consuming task. This explains why formal verification is today an active research area. Interesting results are now available for timed automata formal verification. For this class of models, the tool UPPAAL allows to verify automatically timed properties. With this work we allow to take advantage of results obtained on timed automata and to apply them to perform formal verification of GRAFCET models. In order to apply this technique a translation algorithm that allows to express automatically the behavior of a GRAFCET model with a timed automaton has been carried out.
Sommario
L’obiettivo di questa tesi è dare un contributo nel risolvere il problema della verifica formale di modelli descritti in termini di GRAFCET con vincoli temporali. Il GRAFCET è un modello grafico standardizzato usato per descrivere il comportamento di sistemi logici sequenziali. Attualmente, tutte le soluzioni offerte agli ingegneri per effettuare la verifica formale di modelli GRAFCET sono basate su tecniche di simulazione. In ogni caso la generazione di sequenze per la simulazione è un processo incline all’errore, noioso e dispendioso in termini di tempo. Questo spiega perché la verifica formale al giorno d’oggi è un’attiva area di ricerca. Attualmente sono disponibili interessanti risultati riguardo la verifica formale degli automi temporizzati. Per questa classe di modelli l’applicazione UPPAAL permette di verificare automaticamente le proprietà temporali. Grazie ai risultati di questo lavoro, è possibile sfruttare i vantaggi ottenuti sugli automi temporizzati e applicarli per effettuare la verifica formale di modelli GRAFCET. Per utilizzare queste tecniche, è stato realizzato un algoritmo che consente di esprimere in modo automatico il comportamento di un modello GRAFCET in termini di automa temporizzato.