Abstract: In this study, formal methods are applied for topological analysis of railway network and connectivity of trains, in modeling of moving block railway interlocking system. As, at the current stage of development, in formal methods there does not exits any single formal approach which can be used for the development of a complex system, that is why graph theory is integrated with VDM-SL to achieve this objective. For domain modeling, it is analyzed that a train must respect the topology at switches and crossings. At first, the track segments occupied by a train are searched and then the following properties are formalized: (i) the track segments occupied by a train must be a path in the topology, (ii) the path generated must respect the topology at switches and (iii) the path must respect the topology at railway crossing. Formal specification of the system is described using VDM-SL and the model is validated using VDM-SL toolbox.