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

被引：3
作者：
School of Electronics and Information Engineering, Tongji University, No. 4800 Cao'an Highway, Shanghai, China [1 ]
机构：
[1] School of Electronics and Information Engineering, Tongji University, Shanghai
来源：
Meng, M. (mei_meng@163.com) | 1600年 / Inderscience Enterprises Ltd., 29, route de Pre-Bois, Case Postale 856, CH-1215 Geneva 15, CH-1215, Switzerland卷 / 46期
关键词：
Labelled transition system; LTS; Model checking; RSSP; Safety;
D O I：
10.1504/IJCAT.2013.052795
中图分类号：
学科分类号：
摘要：
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. Copyright © 2013 Inderscience Enterprises Ltd.
引用
收藏
页码：195 / 202
页数：7
相关论文
共 15 条
  • [1] Alpern B., Schneider F.B., Defining liveness, Information Processing Letters, 21, 4, pp. 181-185, (1985)
  • [2] Cheung S.C., Kramer J., Checking safety properties using compositional reachability analysis, ACM Transactions on Software Engineering and Methodology, 8, 1, pp. 49-78, (1999)
  • [3] Corbett J.C., Avrunin G.S., Using integer programming to verify general safety and liveness properties, Formal Methods System. Des., 6, 1, pp. 97-123, (1995)
  • [4] Frei R., Serugendo G.D.M., Concepts in complexity engineering, International Journal of Bio-inspired Computing, 3, 2, pp. 123-139, (2011)
  • [5] Frei R., Serugendo G.D.M., Advances in complexity engineering, International Journal of Bio-inspired Computing, 3, 4, pp. 199-212, (2011)
  • [6] Green D.G., Elements of a network theory of complex adaptive systems, International Journal of Bio-inspired Computing, 3, 3, pp. 159-167, (2011)
  • [7] Functional Safety of Electrical/Electronic/Programmable Electronic Safety-Related Systems, (1998)
  • [8] Railway Applications -Communication, Signal and Processing Systems. Part 1: Safetyrelated Communications in Closed Transmission System, (2002)
  • [9] Khalgui M., Mosbahi O., Formal approach for the development of intelligent industrial control components, International Journal of Computer Applications in Technology, 42, 2-3, pp. 84-107, (2011)
  • [10] Lee J.H., Hwang J.G., Park G.T., Performance evaluation and verification of communication protocol for railway signaling systems, Computer Standards &Interfaces in Elsevier, 27, pp. 205-219, (2005)
12