首页|Analysing an autonomous tramway positioning system with the UPPAAL Statistical Model Checker

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

扫码查看
The substitution of traditional occupancy detecting sensors with an Autonomous Positioning System (APS) is a promising solution to contain costs and improve performance of current tramway signalling systems. APS is an onboard system using satellite positioning and other inertial platforms to autonomously estimate the position of the tram with the needed levels of uncertainty and protection. However, autonomous positioning 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 proposed, and it is analysed using Uppaal Statistical Model Checker. A novel model-driven hazard analysis approach to the exploration of emerging hazards is proposed. The analysis emphasises how the virtualisation of legacy track circuits and on-board satellite positioning equipment may give rise to new hazards, not present in the traditional system.

RailwaySignallingStatistical model checkingUppaalAutonomouspositioning system

Basile, Davide、Fantechi, Alessandro、Rucher, Luigi、Mando, Gianluca

展开 >

CNR, Inst Informat Sci & Technol Alessandro Faedo ISTI, Pisa, Italy

Univ Florence, Dept Informat Engn, Florence, Italy

Thales Italia SpA, Florence, Italy

2021

Formal aspects of computing

Formal aspects of computing

EISCI
ISSN:0934-5043
年,卷(期):2021.33(6)
  • 4
  • 59