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 条

[21]

Zhang X.M., Liu H.X., Zhao Y.Q., Communication technology in two out of two computer interlocking system, China Railway Science, 26, 5, pp. 96-100, (2005)

[22]

Wang X., Ma L.C., Yuan B.B., Design and implementation of 2 * 2 out of 2 safety computer platform, Urban Rapid Rail Transit, 24, 4, pp. 17-21, (2011)

[23]

Duan W., Computer Interlocking System, (2015)

[24]

Magee J., Kramer J., Concurrency State Models and Java Programs, (1999)

← 1 2 3 →