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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- M. Ghazel, “Formalizing a Subset of ERTMS/ETCS Specifications for Verification Purposes,” Transportation Research Part C, No. 42, pp. 60-75, 2014
- 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
- 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
- W. Duan, “Computer Interlocking System,” China Railway Publishing House, Beijing, 2015
- 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.
Attachments:
IJPE-2018-11-22.pdf | [Formal Verification of Double Two out of Two Computer Systems] | 578 Kb |
|