Statistical model checking of hazards in an autonomous tramway positioning system

One promising option to improve performance and contain costs of current tramway signalling systems is to introduce an Autonomous Positioning System (APS) in substitution of traditional occupancy detecting sensors. APS is an onboard system that uses a plurality of sensors (such as GPS or inertial platform) and a Sensor Fusion Algorithm (SFA) to autonomously estimate the position of the tram with the needed levels of uncertainty and protection. Autonomous positioning however introduces, even in absence of faults, a quantitative uncertainty with respect to traditional sensors. This paper investigates this issue in the context of an industrial project: a model of the envisaged solution is adopted, and the Uppaal Statistical Model Checker is used to study possible hazards induced by the substitution of legacy track circuits with on-board satellite positioning equipment.