Formal methods-based design of dynamically configurable traffic lights management systems

The goal of this thesis is to create a method for the development of reconfigurable traffic lights management systems that facilitates the creation and analysis of the controlling rules. The method should be based on high-level notations, that can be used by domain experts to easily manage traffic signals, guaranteeing more flexibility and safety at the same time. The development of new rules for the management of traffic signals must be easy and fast, providing an intuitive mechanism for modelling new rules and a testing environment able to analyse them. To achieve these goals, this work follows an approach based on two levels. The first one is a high-level description of the system, performed by using the UML formalism, with the definition of all the objects and their attributes. The second level is a formal model, based on timed automata, that is used to build and analyse the logical sequence and the timing of traffic lights of a crossroad. The rules used in this level have been created from scratch, modelled using the timed automata formalism and they have been implemented in the UPPAAL formal verification tool. The approach presented in this thesis allows users to create, simulate and verify the behaviour of a whole network of crossroads, starting from the lower level of the single traffic signal, passing through the sequence, or algorithm, that manages single nodes, up to a higher level that can control requests regarding more than one node per time, like the green wave. Finally, this work outlines a procedure to automatically generate UPPAAL models from the original UML.

L’obiettivo di questa tesi è di creare un metodo per lo sviluppo di un sistema di controllo per semafori riconfigurabili, che facilita la creazione e l’analisi delle regole di controllo. Il metodo è basato su istruzioni di alto livello, che possono essere usate da esperti di dominio per gestire con facilità i semafori, garantendo sia flessibilità che sicurezza. Lo sviluppo di nuove regole per la gestione dei semafori deve essere facile e veloce, fornendo un meccanismo intuitivo per la modellazione di nuove regole e un ambiente di prova dove poterle testare ed analizzare. Per raggiungere questi obiettivi, questo lavoro segue un approccio basato su due livelli. Il primo è una descrizione di alto livello del sistema, utilizzando il formalismo UML, con la definizione di ogni oggetto e dei suoi relativi attributi. Il secondo livello è un modello formale, basato su automi temporizzati, utilizzato per costruire ed analizzare la sequenza logica e le tempistiche dei semafori di un incrocio. Le regole utilizzate in questo livello sono state create da zero, modellate tramite il formalismo degli automi temporizzati e implementate nello strumento di verifica formale UPPAAL. L’approccio presentato in questa tesi permette all’utente di creare, simulare e verificare il comportamento di una rete di incroci, partendo dal livello più basso, ovvero il semaforo, passando per la sequenza, o algoritmo, che controlla il singolo incrocio, fino al livello più alto che gestisce richieste riguardanti più di un incrocio per volta, come le onde verdi. Infine questo lavoro delinea una procedura per generare automaticamente modelli UPPAAL partendo dall’UML originale.