Author(s)

WANG KEMING, WANG ZHENG, ZHANG CHUANDONG

Abstract

Railway interlocking system is a typical safety-critical system, design defects of the system will pose the great risks on the safety and affect the operation efficiency of the railway station. Formal method is an important approach to verify the design requirement and to get the reliable logic for coding. By analysing the requirement of railway interlocking system, the properties of specification and the events of system’s function were obtained, and then a multilayer formal model using the Event-B language and refinement strategy was established. The safety attributes of the system were verified and the formal model was refined based the theorem proving. Taking a real railway station as example, the contradictions of the axioms and the deadlock of the model were checked, as well as the correctness of the interlocking data was validated. Finally, the correctness of the model function was tested by simulation. We developed a formal prototype model for the general interlocking system and proposed an approach of data validation for the real station with the interlocking table.

Keywords

railway signalling system, station interlocking, formal modelling, data validation, theorem proving, model checking, simulation