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 thus are 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 (RBD) have been used to model the reliability of the 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 (HOL) theorem proving to carry out an accurate reliability analysis of a railway system
designed for the Italian High Speed Railways.

Proof Script: TBA

Waqar Ahmad is a PhD student at the School of Electrical Engineering and Computer Science of National University of Sciences and Technology. He is working on his PhD thesis in the System Analysis & Verification (SAVE) Lab of NUST-SEECS, under the supervision of Dr. Osman Hasan.