A Systematic Approach for Determining and Verifying Hazards to Support ETCS Moving Block Safety Assessment

Moving Block (MB) railway signalling enhances railway capacity through dynamic train separation based on realtime localisation and braking distances. These complex functional behaviours of MB systems, such as communication processes, and timing constraints, make safety assessment particularly challenging. Formal verification techniques, in particular model checking, are increasingly adopted in industry to prove the correctness of such safety-critical systems. However, to cope with the state explosion problem, verification models are often simplified, reducing their accuracy and limiting their applicability to realistic operational conditions. To address this limitation, we propose an integrated verification approach combining System-Theoretic Process Analysis (STPA) and Statistical Model Checking (SMC). STPA is used to identify relevant causal factors and hazardous operational scenarios, including disturbances such as delays and sensor errors, which are then explicitly incorporated into the formal model. Safety properties are subsequently analysed under these realistic conditions using UPPAAL SMC.

Keywords: Safety Analysis, Moving Block, Railway Signalling, Statistical Model Checking, STPA, UPPAAL.