Formal Fault Tree based Dependability Analysis of Railway Level Crossing using Theorem Proving

Abstract: Safety assurance in the railways is a dire requirement due to the involvement of human lives and high financial costs. It has been identified that a majority of the accidents in railways occur at level crossings, i.e., the intersection between railway and road traffic. Traditionally, Fault Tree (FT) method has been used to develop the failure models for railway level crossings by considering the failure characteristics of the corresponding signaling system. These resulting failure models are then analyzed using paper-and-pencil methods or computer simulations but they cannot assure accurate analysis results due to their inherent limitations. As an accurate alternative, we propose to use higher-order logic theorem proving for conducting the formal FT-based dependability analysis, i.e., failure and unavailability, of signaling system at railway level crossing. The paper presents a formal approach for this purpose besides some ML-based tactics that allow automatically computing the failure and unavailability probability of signaling systems at railway level crossings for practical purposes. For illustration, we present the formal FT-based dependability analysis of a signaling system at a Moroccan level crossing by considering the failures of power and communication networks, control and operative system components.