Modellazione e simulazione di un sistema intelligente di controllo dei semafori a Berlino utilizzando UPPAAL-SMC e dati di traffico reali.

Abstract

I sistemi convenzionali di controllo del traffico sono progettati principalmente per massimizzare il flusso veicolare, spesso a scapito della sicurezza dei pedoni e degli altri utenti vulnerabili della strada. Questa tesi sviluppa un quadro formale basato sui dati per la progettazione e la validazione di una logica di controllo del traffico basata sulla priorità. La soluzione proposta consiste nel modellare gli incroci stradali come sistemi dinamici stocastici, in cui le transizioni tra le fasi sono controllate da soglie di ingresso in tempo reale, calibrate sul dataset Berlin MeTS-10. La verifica statistica del modello (SMC) nell'ambiente UPPAAL Stratego viene utilizzata per valutare le variabili di prestazione e sicurezza del controllore in condizioni urbane incerte. Il metodo viene testato utilizzando un caso di studio di un incrocio ad alta densità a Berlino. I risultati mostrano che la strategia di priorità preventiva garantisce stabilità operativa e rigoroso rispetto delle norme di sicurezza anche in scenari di picco di traffico intenso e disturbi imprevisti. Il lavoro contribuisce allo sviluppo dell'infrastruttura di trasporto intelligente combinando la verifica matematica formale con dati empirici sulla mobilità urbana per garantire algoritmi di controllo affidabili e "sicuri fin dalla progettazione". Il lavoro contribuisce al progresso di un'infrastruttura di trasporto intelligente affidabile e "sicura fin dalla progettazione" integrando la verifica matematica formale con dati empirici sulla mobilità urbana. Parole chiave: Controllo semaforico urbano, UPPAAL Stratego, Verifica statistica del modello, Dati aperti di Berlino, MeTS-10, Mobilità urbana, Sicurezza pedonale, Analisi di resilienza.

Conventional traffic control systems are primarily designed to maximize vehicle throughput, often at the expense of the safety requirements for pedestrians and other vulnerable road users. This thesis develops a formal data-driven framework for the design and validation of priority-based traffic control logic. The solution is that we propose models of traffic intersections as stochastic dynamic systems, where the transitions between phases are controlled by real-time entry thresholds, calibrated on the Berlin MeTS-10 dataset. Statistical model checking (SMC) in UPPAAL Stratego environment is used to evaluate the performance and safety variables of the controller in uncertain urban conditions. The method is tested using a case study of a high-density intersection in Berlin. The results show that the priority- preemptive strategy guarantees operational stability and strict safety compliance even under severe peak load scenarios and unexpected disturbances. The work contributes to the development of the intelligent transportation infrastructure by combining formal mathematical verification with empirical urban mobility data to assure reliable, “safe-by-design” control algorithms. The work contributes to the advancement of reliable, “safe-by-design” intelligent transport infrastructure by integrating formal mathematical verification with empirical urban mobility data. Keywords: Urban Traffic Signal Control, UPPAAL Stratego, Statistical Model Checking, Berlin Open Data, MeTS-10, Urban Mobility, Pedestrian Safety, Resilience Analysis.