Formal verification of double two out of two computer systems

被引：2

作者：

Feng H. ^{[1
,2
]}

Ma X. ^{[3
]}

Fu W. ^{[1
,2
]}

Pan M. ^{[1
,2
]}

机构：

[1] Signal and Communication Research Institute, China Academy of Railway Sciences Corporation Limited, Beijing

[2] Center of National Railway Intelligent Transportation System Engineering and Technology, Beijing

[3] China Railway Test and Certification Center, Beijing

来源：

International Journal of Performability Engineering | 2018年 / 14卷 / 11期

关键词：

Double two out of two computer system; Formal verification; Labelled transit system; Model checking; Safety critical system;

D O I：

10.23940/ijpe.18.11.p22.27602768

中图分类号：

学科分类号：

摘要：

The double two out of two safety computer system is widely used in China’s rail transit. To enhance the safety integrity level of such a system, safety related logic is described and modelled by FSP (finite state process) language in a simple and explicit manner. A new method based on LTS (labelled transition system) model checking is proposed for verifying the system safety properties. The LTS method is adapted to model system behaviors by means of LTSA (labelled transition system analyzer) software. It visualizes overall activity traces and is easy for analysis and safety verification by developers. Simulation and verification results indicate that the LTS method provides great assistance for designers to develop more efficient and reliable complex systems. © 2018 Totem Publisher, Inc. All rights reserved.

引用

页码：2760 / 2768

页数：8

共 24 条

[1]

Ning B., Liu C., Technology and application of train operation control system for China rail transit system, Journal of The China Railway Society, 39, 2, pp. 1-9, (2017)

[2]

Guo Z.L., Gao C.H., Ma L.C., Lv J.D., Formal Verification of Safety Computer Platform based on Timed Automata Model, Journal of The China Railway Society, 33, 6, pp. 68-73, (2011)

[3]

Cao Y., Tang T., Xu T.H., Mu J.C., Application of formal methods in train control system, Journal of Traffic and Transportation Engineering, 10, 1, pp. 112-126, (2010)

[4]

Liu J.T., Tang T., Zhao L., Liu L., Functional Safety Analysis of CTCS-3 Train Control System based on Control Relationship Model, Journal of The China Railway Society, 37, 8, pp. 36-43, (2015)

[5]

Yu L.Z., Xu Z.W., Chen Z.X., Zhang S.Q., Formal Verification of Railway Interlocking System based on Ladder Logic, Journal of Computer Applications, 33, 12, pp. 3419-3422, (2013)

[6]

Chen G.W., Fan D.W., Wei Z.S., Fang Y.F., All Electronic Computer Interlocking System based on Double 2 Vote 2, China Railway Science, 31, 4, pp. 138-144, (2010)

[7]

Wang X., Ma L.C., Tang T., Study on formal modeling and verification of safety computer platform, Advances in Mechanical Engineering, 8, 5, pp. 1-13, (2016)

[8]

Lu J.D., Tang T., Yan F., Xu T.H., UPPAAL-based Simulation and Verification of CBTC Zone Control Subsystem in Rail Transportation, Journal of The China Railway Society, 31, 3, pp. 59-64, (2009)

[9]

Chen M.S., Bao Y.X., Sun H.Y., Miao W.K., Chen X.H., Zhou T.L., Survey on Formal Method of Trustworthy Construction for Communication-based Train Control Systems, Journal of Software, 28, 5, pp. 1183-1203, (2017)

[10]

Zafar N., Formal dynamic operational model of rIS components, International Journal of Computer Science and Network Security, 11, 9, pp. 91-97, (2011)

← 1 2 3 →