Formal Reliability Analysis of Railway Systems Using Theorem Proving Technique

Abstract

Railways provide a cost- and energy-efficient way to transport goods by means of high-speed trains and are thus an integral part of the international trade and economic growth in most countries. A traction drive system, consisting of many electrical devices, is primarily utilized to ensure high speeds in modern trains. Due to the safety-critical nature of these high-speed trains, a rigorous reliability analysis of the railway traction drive system is highly desired. Traditionally, reliability block diagrams have been used to model the reliability of high-speed trains, which are then analyzed using paper-and-pencil proof methods and computer simulations. However, both of these reliability analysis methods cannot guarantee absolute correctness due to their inherent inaccuracy limitations. As a promising alternative, we propose to use higher-order logic theorem proving to carry out an accurate reliability analysis of a railway system designed for the Italian high-speed railways.