Analysing an autonomous tramway positioning system with the Uppaal Statistical Model Checker

The substitution of traditional occupancy detecting sensors with anAutonomous Positioning System (APS) is a promising solution tocontain costs and improve performance of current tramway signallingsystems. APS is an onboard system using satellite positioning andother inertial platforms to autonomously estimate the position ofthe tram with the needed levels of uncertainty and protection.However, autonomous positioning introduces, even in absence offaults, a quantitative uncertainty with respect to traditionalsensors. This paper investigates this issue in the context of anindustrial project: a model of the envisaged solution is proposed,and it is analysed using Uppaal Statistical Model Checker.A novel model-driven hazard analysis approach to the exploration ofemerging hazards is proposed. The analysis emphasises how thevirtualisation of legacy track circuits and on-board satellitepositioning equipment may give rise to new hazards, not present inthe traditional system.