Formal Verification of Double Two out of Two Computer Systems

doi:10.23940/ijpe.18.11.p22.27602768

Int J Performability Eng ›› 2018, Vol. 14 ›› Issue (11): 2760-2768.doi: 10.23940/ijpe.18.11.p22.27602768

Previous Articles Next Articles

Formal Verification of Double Two out of Two Computer Systems

Haonan Feng^{a, b, *}, Xiaojiao Ma^c, Wei Fu^{a, b}, and Ming Pan^{a, b}

^a Signal and Communication Research Institute, China Academy of Railway Sciences Corporation Limited, Beijing, 100081, China;
^b The Center of National Railway Intelligent Transportation System Engineering and Technology, Beijing, 100081, China;
^c China Railway Test and Certification Center, Beijing, 100081, China

Submitted on ;
Contact: * E-mail address: fenghaonan@rails.cn
About author:Haonan Feng is a senior engineer in the Signal and Communication Research Institute at China Academy of Railway Sciences Corporation Limited, China. His research interests include formal method and software verification.Xiaojiao Ma is an assistant professor in the China Railway Test and Certification Center, China. Her research interests include formal method and software verification.Wei Fu is an associate professor in the Signal and Communication Research Institute at China Academy of Railway Sciences Corporation Limited, China. His research interests include formal method and software verification.Ming Pan is an associate professor in the Signal and Communication Research Institute at China Academy of Railway Sciences Corporation Limited, China. His research interests include computer interlocking system development.

Abstract

Abstract: 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.

Key words: safety critical system, labelled transit system, double two out of two computer system, model checking, formal verification

Haonan Feng, Xiaojiao Ma, Wei Fu, and Ming Pan. Formal Verification of Double Two out of Two Computer Systems [J]. Int J Performability Eng, 2018, 14(11): 2760-2768.

Add to citation manager EndNote|Reference Manager|ProCite|BibTeX|RefWorks

References

[1] B. Ning and C. Liu, “Technology and Application of Train Operation Control System for China Rail Transit System,” Journal of the China Railway Society, Vol. 39, No. 2, pp. 1-9, 2017
[2] Z. L. Guo, C. H. Gao, L. C. Ma,J. D. Lv, “Formal Verification of Safety Computer Platform based on Timed Automata Model,” Journal of the China Railway Society, Vol. 33, No. 6, pp. 68-73, 2011
[3] Y. Cao, T. Tang, T. H. Xu,J. C. Mu, “Application of Formal Methods in Train Control System,” Journal of Traffic and Transportation Engineering, Vol. 10, No. 1, pp. 112-126, 2010
[4] J. T. Liu, T. Tang, L. Zhao,L. Liu, “Functional Safety Analysis of CTCS-3 Train Control System based on Control Relationship Model,” Journal of the China Railway Society, Vol. 37, No. 8, pp. 36-43, 2015
[5] L. Z. Yu, Z. W. Xu, Z. X. Chen,S. Q. Zhang, “Formal Verification of Railway Interlocking System based on Ladder Logic,” Journal of Computer Applications, Vol. 33, No. 12, pp. 3419-3422, 2013
[6] G. W. Chen, D. W. Fan, Z. S. Wei,Y. F. Fang, “All Electronic Computer Interlocking System based on Double 2 Vote 2,” China Railway Science, Vol. 31, No. 4, pp. 138-144, 2010
[7] X. Wang, L. C. Ma,T. Tang, “Study on Formal Modeling and Verification of Safety Computer Platform,” Advances in Mechanical Engineering, Vol. 8, No. 5, pp.1-13, 2016
[8] J. D. Lü, T. Tang, F. Yan,T. H. Xu, “UPPAAL-based Simulation and Verification of CBTC Zone Control Subsystem in Rail Transportation,” Journal of the China Railway Society, Vol. 31, No. 3, pp. 59-64, 2009
[9] M. S. Chen, Y. X. Bao, H. Y. Sun, W. K. Miao, X. H. Chen,T. L. Zhou, “Survey on Formal Method of Trustworthy Construction for Communication-based Train Control Systems,” Journal of Software, Vol. 28, No. 5, pp. 1183-1203, 2017
[10] N. Zafar, “Formal Dynamic Operational Model of RIS Components,” International Journal of Computer Science and Network Security, Vol. 11, No. 9, pp. 91-97, 2011
[11] H. D. Tong, B. Ning,H. F. Wang, “Research on Event-B based Modelling and Verification of Interlocking Route Control,” Railway Computer Application, Vol. 22, No. 6, pp. 57-61, 2013
[12] N. Zafar, “Formal Model for Moving Block Railway Interlocking System based on Un-Directed Topology,” inProceedings of the 2nd International Conference on Emerging Technologies, pp. 217-223, 2006
[13] H. Song, J. Liu,E. Schnieder, “Validation, Verification and Evaluation of a Train to Train Distance Measurement System by Means of Colored Petri Nets,”Reliability Engineering & System Safety, No. 164, pp. 10-23, 2017
[14] E. Schnieder, L. Schnieder,J. R. Mueller, “Conceptual Foundation of Dependable Systems Modeling,” in Proceedings of the 2nd IFAC Workshop on Dependable Control of Discrete System, Vol. 2, No. 1, pp. 198-202, 2009
[15] M. M. Z.Hörste and E. Schnieder, “Modelling and Simulation of Train Control Systems Using Petri Nets,” inProceedings of International Symposium on Formal Methods, pp. 1867-1883, 1999
[16] Y. Dong and X. J. Gao, “Method for Generating Formal Interlocking Software Model based on Scenario,” Computer Science, Vol. 42, No. 1, pp. 193-195, 2015
[17] X. Y. Zhao, R. J. Cheng, Y. Cheng,X. P. Ma, “Formal Modeling and Parameter Analysis Method for Train Control System based on Hybrid Unified Modeling Language,” Journal of the China Railway Society, Vol. 38, No. 11, pp. 80-87, 2016
[18] X. Wang, Z. W. Xu,M. Mei, “A Software Safety Verification Method based on Model Checking,” Journal of Wuhan University (Natural Science Edition), Vol. 56, No. 2, pp. 156-160, 2010
[19] M. Mei, Z. W. Xu, X. Wang,Y. B. Wan, “Model Checking-based Safety Verification for Railway Signal Safety Protocol-I,” International Journal of Computer Applications in Technology, Vol. 46, No. 3, pp. 195-202, 2013
[20] M. Ghazel, “Formalizing a Subset of ERTMS/ETCS Specifications for Verification Purposes,”Transportation Research Part C, No. 42, pp. 60-75, 2014
[21] X. M. Zhang, H. X. Liu,Y. Q. Zhao, “Communication Technology in Two out of Two Computer Interlocking System,” China Railway Science, Vol. 26, No. 5, pp. 96-100, 2005
[22] X. Wang, L. C. Ma,B. B. Yuan, “Design and Implementation of 2 * 2 out of 2 Safety Computer Platform,” Urban Rapid Rail Transit, Vol. 24, No. 4, pp. 17-21, 2011
[23] W. Duan, “Computer Interlocking System,” China Railway Publishing House, Beijing, 2015
[24] J. Magee and J. Kramer, “Concurrency State Models and Java Programs,” John Wiley Sons Ltd., Chichester, 1999

Formal Verification of Double Two out of Two Computer Systems

PDF

Knowledge

Abstract

Cite this article

share this article

References

Related Articles 1

Recommended 0