Title: Model checking-based safety verification for railway signal safety protocol-I

Authors: Mei Meng; Xu Zhongwei; Wang Xi; Wan Yongbing

Addresses: School of Electronics and Information Engineering, Tongji University, No. 4800 Cao'an Highway, Shanghai, China ' School of Electronics and Information Engineering, Tongji University, No. 4800 Cao'an Highway, Shanghai, China ' School of Electronics and Information Engineering, Tongji University, No. 4800 Cao'an Highway, Shanghai, China ' School of Electronics and Information Engineering, Tongji University, No. 4800 Cao'an Highway, Shanghai, China

Abstract: RSSP-I is one kind of safety communication protocol in signal system of China high-speed railways, which is needed to be verified in safety properties while assessing the whole system. Model checking is an effective way for verifying the safety properties of communication protocols. This paper proposes a new method based on labelled transition system (LTS) model checking for verifying the safety communication protocol's safety properties. First, it retrieves the safety requirement of RSSP-I, then adopts LTS to model the interaction behaviours in the system, after that, it analyses and verifies the safety properties of the model by means of LTSA (LTS analyser). The result of verification illustrates that the method can be efficiently applied to safety properties verification of protocol. Moreover, the method can be used to improve the designing and developing the safety protocols as well.

Keywords: model checking; labelled transition system; LTS; safety verification; railway signal safety; safety protocols; RSSP; railway signalling; high-speed railways; China; communication protocols; safety communication.

DOI: 10.1504/IJCAT.2013.052795

International Journal of Computer Applications in Technology, 2013 Vol.46 No.3, pp.195 - 202

Published online: 29 May 2013 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article