Xiaochun Wu1, Xiang Zhou This email address is being protected from spambots. You need JavaScript enabled to view it.1 and Yayun Luo2
1School of Automation & Electrical Engineering, Lanzhou Jiao Tong University, Lanzhou 730070, P.R. China 2Yinchuan Communication and Signal Division of Lanzhou Railway Bureau, Yinchuan 750001, P.R. China
Received: June 23, 2016 Accepted: October 4, 2016 Publication Date: March 1, 2017
Temporary speed restriction server (TSRS) is an important part of the high speed railway train control system, TSRS not only needs to check the temporary speed restriction orders issued by CTC, but also needs to exchange information frequently with temporary speed restriction server of adjacent dispatching station, on this account TSRS has higher requirements for security and real time property. In order to satisfy the real-time requirements, timed automata sub-models of each equipment are established for the working process of cross-border temporary speed restriction, and the overall timed automata network modelsare built through parallel composition of the sub-models. The BNF (backus-naur form) syntax is used to describe the properties of the cross-border temporary speed restriction server, and the verification tool of UPPAAL is used to simulate the models. The verification results confirm the safety and bounded liveness properties of the system in the interaction process.
[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).
[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)
[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).
[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).
[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)
[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)
[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)
[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)
[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)
[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)
[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).
[13] Cao, Y., Research on Formal Modeling and Verification Method of High Speed Railway Train Operation Control System, Beijing: Beijing Jiaotong University (2011). (Chinese)
[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)
We use cookies on this website to personalize content to improve your user experience and analyze our traffic. By using this site you agree to its use of cookies.
