Abstract

Since the railway system is concurrent, distributed, safety, monetary and environmental critical system. Its failure may cause the loss of human life, severe injuries, loss of money and environmental issues. The complexity of the system requires formal modeling and step by step design processes. In this paper, we present a method of modeling and analysis of railway crossing, which is an important and critical component of the moving block railway interlocking system. For this purpose, Petri net (PN) formalism is used to model the safety requirements of trains. Furthermore, due to the continuous and inexact features like speed and stopping distance, intelligent braking system is required to stop the train in order to achieve full safety and comfort during its braking. To alleviate this issue, we use fuzzy inference system based on input values, that is., speed and crossing distance and calculate the required braking strength. Moreover, this paper uses reachability graph (RG) to verify the correspondence between the crossing system and its PN representation. 

Key words: Formal methods, Petri net, fuzzy logic, moving block railway interlocking system, safety properties.