DOI: 10.3724/SP.J.1087.2013.03419

Journal of Computer Applications (计算机应用) 2013/33:12 PP.3419-3422

Formal verification of railway interlocking system based on ladder logic

Ladder logic was used to model the railway interlocking system. In order to achieve the purpose of formal verification of the railway interlocking system, the model of the railway interlocking system expressed by ladder logic was converted to NuSMV language, which was a temporal logic model checker. Then Computational Tree Logic (CTL) specification representing the safety requirements of the railway interlocking system was verified. Finally, the formal verification of computer design model of the railway interlocking system was implemented based on NuSMV.

Key words:railway interlocking system,model checking,formal method,ladder logic,NuSMV model checking

ReleaseDate:2014-07-21 16:59:15