Integrating DSL-CBI and NuSMV for Modeling and Verifiying Interlocking Systems

The Computer Based Interlocking System (CBI) is used to ensure safe train movements at a railway station. For a given station, all the train routes and the concrete safety rules associated with these are defined in the interlocking table. Currently, the development and verification of interlocking tables is entirely manual process, which is inefficient and error-prone due to the complexity of the CBI and the human interferences. Besides, the complexity and volume of the verification results tend to make users feel extremely non-understandable. In order to tackle these problems, we introduce a toolset based on Domain Specific Language for Computer Based Interlocking Systems (DSL-CBI) to automatically generate and verify the interlocking table, and then mark the conflicting routes in the railway station. In this paper, we also discuss the advantages of the toolset and the significant contribution in developing CBI based on the proposed toolset.