Username   Password       Forgot your password?  Forgot your username? 

 

Formal Verification of Double Two out of Two Computer Systems

Volume 14, Number 11, November 2018, pp. 2760-2768
DOI: 10.23940/ijpe.18.11.p22.27602768

Haonan Fenga,b, Xiaojiao Mac, Wei Fua,b, and Ming Pana,b

aSignal and Communication Research Institute, China Academy of Railway Sciences Corporation Limited, Beijing, 100081, China
bThe Center of National Railway Intelligent Transportation System Engineering and Technology, Beijing, 100081, China
cChina Railway Test and Certification Center, Beijing, 100081, China

(Submitted on August 4, 2018; Revised on September 11, 2018; Accepted on October 25, 2018)

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.

 

References: 24

                  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, and 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, and 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, and 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, and 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, and 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, and 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, and 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, and 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, and 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,” in Proceedings of the 2nd International Conference on Emerging Technologies, pp. 217-223, 2006
                  13. H. Song, J. Liu, and 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, and 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,” in Proceedings 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, and 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, and 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 , and 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, and 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, and 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

                                   

                                  Please note : You will need Adobe Acrobat viewer to view the full articles.Get Free Adobe Reader

                                  Attachments:
                                  Download this file (IJPE-2018-11-22.pdf)IJPE-2018-11-22.pdf[Formal Verification of Double Two out of Two Computer Systems]578 Kb
                                   
                                  This site uses encryption for transmitting your passwords. ratmilwebsolutions.com