Modeling and Verification of Cross-Border Temporary Speed Restriction for High Speed Railway Train Control System Based on UPPAAL

Xiaochun Wu¹, Xiang Zhou This email address is being protected from spambots. You need JavaScript enabled to view it.¹ and Yayun Luo²

¹School of Automation & Electrical Engineering, Lanzhou Jiao Tong University, Lanzhou 730070, P.R. China
²Yinchuan Communication and Signal Division of Lanzhou Railway Bureau, Yinchuan 750001, P.R. China

REFERENCES

1. [1] Wu, Y. G. and Lu, H. J., “Modeling and Verification of Real-time System Based on Timed Automata,” Computer Age, Vol. 6, No. 1, pp. 23 (2011). (Chinese) [2] OLDEROGER, DIERKSH. Real-time System, London: Cambridge University Press, pp. 137146 (2008).
2. [3] Guo, Z., “Discussion on the Application of Temporary Speed Restriction Technology in the System of CTCS,” Scientific and Technological Information, Vol. 16, pp. 111112 (2011). (Chinese)
3. [4] Jiang, M. H., Discussion on Setting Up Temporary Speed Limit Section of the Inter Train Control System, Railway Communication Signal, Vol. 5, No. 4, pp. 32 33 (2013).
4. [5] Liu, C. H. and Zhang, G. Q., “Formal Verification Method for Real-time System Based on Timed Automata Network,” Journal of Soochow University, Vol. 24, No. 1, pp. 3540 (2008).
5. [6] Science and Technology [2010] 137 Number. “Specification for Temporary Speed Restriction of Train Control System for Passenger Dedicated Line (V2.0) [S],” China, (2010). (Chinese)
6. [7] Zhen, L. J., “Research and Application of Temporary Speed Restriction for Passenger Dedicated Line,” Cheng du. University of Electronic Science and Technology of China, pp. 3450 (2012). (Chinese)
7. [8] Yuan, L. and Wang, J. F., “Modeling and Verification of Temporary Speed Limit for CTCS-3 Level Train Control System,” Journal of Southwest Jiao Tong University, Vol. 48, No. 4, pp. 701712 (2013). (Chinese)
8. [9] Kang, R. W., “Modeling and Verification of CTCS-3 Level Train Control System Based on Timed Automata,” Beijing: Beijing Jiaotong University, pp. 40 53 (2013). (Chinese)
9. [10] Shi, S. Y. and Zhang, H., Design of Supply Chain Workflow Model Based on Message Sequence Diagram and Petri Net, Journal of Management, Vol. 4, No. 6, pp. 756766 (2007). (Chinese)
10. [11] Zhao, R. L. and Wang, C. L., “Modeling and Verification of Temporary Speed Restriction System of CTC Boundary in High Speed Railway,” Railway Computer Application, Vol. 23, No. 7, pp. 4347 (2014). (Chinese)
11. [12] Muniz, A. L. N., Andrade, A. M. S. and Lima, G., “Integrating UML and UPPAAL for Designing, Specify and Verifying Component-based Real-time Systems,” Innovation in System & Software Engineering, Vol. 6, No. 12, pp. 2937 (2010).
12. [13] Cao, Y., Research on Formal Modeling and Verification Method of High Speed Railway Train Operation Control System, Beijing: Beijing Jiaotong University (2011). (Chinese)
13. [14] Lv, J. D., Tang, T., Yan, F. and Xu, T. H., “Modeling and Verification of CBTC Regional Control Subsystem of Urban Rail Transit Based on UPPAAL,” Journal of Railway, Vol. 32, No. 3, pp. 5964 (2009). (Chinese)