Model checking-based safety verification for railway signal safety protocol-I Online publication date: Wed, 29-May-2013
by Mei Meng; Xu Zhongwei; Wang Xi; Wan Yongbing
International Journal of Computer Applications in Technology (IJCAT), Vol. 46, No. 3, 2013
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.
Existing subscribers:
Go to Inderscience Online Journals to access the Full Text of this article.
If you are not a subscriber and you just want to read the full contents of this article, buy online access here.Complimentary Subscribers, Editors or Members of the Editorial Board of the International Journal of Computer Applications in Technology (IJCAT):
Login with your Inderscience username and password:
Want to subscribe?
A subscription gives you complete access to all articles in the current issue, as well as to all articles in the previous three years (where applicable). See our Orders page to subscribe.
If you still need assistance, please email subs@inderscience.com
Our Blog 
Follow us on Twitter 
Visit us on Facebook