Formal Analysis of Safety Properties of Railway Interlocking System

Abstract

Railway interlocking is a safety, monetary and environmentally critical sys- tem because its failure may cause serious consequences such as loss of human life, severe injuries, and large scale of environmental damages or consider- able economical penalties. The safety and complexity of this system requires formal modeling and step by step refinement for its construction and devel- opment. Formal methods are approaches, based on the use of mathematical techniques and notations, for describing and analyzing properties of software systems. The main focus of this thesis is to develop a moving block railway interlocking system(MBRIS)to prevent trains from collisions and derailing. Three phases have been used in this development. Initially, we give abstract safety properties to prevent train from collisions and derailing. Then we an- alyze properties and refine by linking the moving block (maximum braking distance including length of a train) with trains. The moving block provides safe braking distance associated with every train. Further, to control the interlocking system we associate computer based control to further refine it. we also address some features, for example, variation of moving block, ap- propriate brake strength, priority of train to pass the network components, compact modularity and reusability. To handle these features, it requires an integration of object oriented formal methods with developed methodolo- gies like multi-agent systems and fuzzy logic. For this purpose we develop fuzzy multi-agent specification language (FMASL) using an integration of Object-Z, fuzzy logic and multi-agent approaches. FMASL has a compact modular design approach which can decompose a system in to a collection of interacting fuzzy based agents. Further, we apply FMASL to railway cross- ing which improves the safety property discussed in previous phase. This approach skilled the train to calculate its moving block based on its speed and weight. Priority can be calculated based on its moving block and stop- ping distance. In third phase, we discuss the drawbacks of two dimensional control of train along the switch and level crossing. For example, in switch the controls of both the train and switch must match for the safe and normal movement otherwise it may cause a derailing. The level crossing is another critical component of the railway interlocking, because of the two dimensional safety requirements due to the road traffic. To model this complex system it requires the approach which supports concurrency, modularity and agent mobility. To achieve the desired goal we integrate mobile agent concepts with Petri net (PN) and develop a mobile Petri net (MPN) which supports both mobility and concurrency. Further, we prove that the collection of different MPNs in a connected network is a PN. MPN has model oriented features which can divide the system in collection of independent components which can act concurrently with mobility of mobile agents. It has both graphical and algebraic behavior with strong abstract verification mechanism. Finally, we apply MPN to the MBRIS along the switch and level crossing to bring it to one dimensional control.