Authors : Nazir A. Zafar and Keijiro Araki
Abstract: The fundamental problem associated with the development of safety critical systems, e.g., railway interlocking system is the verification of safety properties, which requires the use of advanced methodologies. Formal methods, having tool support, increase quality and provide highest confidence in this area. In formalizing moving block railway interlocking system, we analyzed and decomposed it into four aspects, i.e., network topology (static model), network state (dynamic model), trains and controls. After analysis, the components are composed to describe the formal model for the whole system. Connectivity of trains and path description of the position of a train are analyzed in topological requirements. Prevention of collisions and derailing are analyzed in safety requirements. Finally, safety properties preventing collisions and derailing are refined by integrating with the notion of moving block of a train. It is observed that the topological analysis contribute to safety of the system. The railway network is modeled in graph theory. Formal specification is described in VDM-SL and the model is validated using VDM-SL toolbox.
Nazir A. Zafar and Keijiro Araki , 2004. Formalizing Safety Properties Preventing Collisions and Derailing in Moving Block Railway Interlocking System using VDM-SL . Asian Journal of Information Technology, 3: 313-328.