TY  - JOUR
T1  - Connectivity and Path Analysis of Trains in Railway Interlocking System
AU - , Nazir Ahmad Zafar 
JO  - Asian Journal of Information Technology
VL  - 4
IS  - 2
SP  - 211
EP  - 217
PY  - 2005
DA  - 2001/08/19
SN  - 1682-3915
DO  - ajit.2005.211.217
UR  - https://makhillpublications.co/view-article.php?doi=ajit.2005.211.217
KW  - 
AB  - 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.
ER  -