CHEN Yong-gang1， YANG Lu1， WANG Dong2
（1. School of Automation and Electrical Engineering, Lanzhou Jiaotong University, Lanzhou 730070, China； 2. School of Mechanical Engineering, Lanzhou Jiaotong University, Lanzhou 730070, China）
Abstract： The zone control subsystem is a real-time control system, which requests the correctness of the control process. Train tracing scene is an important function of the zone controller (ZC) in the communication based train control (CBTC) system. In the process of deep development and design, to ensure the safety of the system, the system needs to be modeled, simulated and verified to discover the system design flaws. Unified modeling language (UML) is combined with timed automata, and timed automata network models of train-filter and train tracing demarcation-point are established. At the same time, the verification tool of UPPAAL is applied to simulate the system, and verify the requirements of performance and function of system. The results show that the function of train tracing demaraction-point meets the requirements of system safety and limited activity. Therefore, the method is feasible and can be applied to the modeling and verification of other scenes of train control system.
Key words： train tracing; communication based train control (CBTC) system; zone controller (ZC); timed automata; UPPAAL
CLD number： U283.2 Document code： A
Article ID： 1674-8042（2019）02-0157-11 doi： 10.3969/j.issn.1674-8042.2019.02.008
References
［1］Tang T, Gao C M, Huang Y N. CJ/T407-2012 Technical requirements of train automatic control System of urban rail transit based on communication. Beijing： China Standard Press, 2012.
［2］Liu J T, Tang T, Zhao L. Modeling and verification of radio block center handover protocol based on differential dynamic logic. Journal of China Railway Science, 2012, 33(5)： 98-104.
［3］Lü J D, Tang T, Yan F, et al. Modeling and verification of CBTC regional control subsystem of urban transit based on UPPAAL. Journal of Railway, 2009, 32(3)： 59-64.
［4］Bowen J. Formal methods in safety-critical standards. Computer, 1993, 27(8)： 68-71.
［5］EN50129-1999 Railway applications： safety related electronic systems for signaling. Beijing： China Standard Press, 1999.
［6］Liu J T, Tang T, Xu T H, et al. Formal verification of CTCS-3 system requirements specification based UML model. Journal of China Railway Science, 2011, 33(3)： 93-99.
［7］Lü J D. Hierarchical formal modeling and verification train control system. Beijing： Beijing Jiaotong University, 2011.
［8］Du J W, Xu Z W, Wang S M. Formal verification of CTCS-3 system requirements specification based UML model. Computer Engineering and Applications, 2007, 43(2)： 1-4.
［9］Hermanns H, Jansen D N, Usenko Y S. From StoCharts to MoDeST： a comparative reliability analysis of train radio communications. In： Proceedings of the 5th International Workshop on Software and Performance, ACM, 2005： 13-23.
［10］Trowitzsch J, Zimmermann A. Using UML state machines and petri nets for the quantitative investigation of ETCS. In： Proceedings of the 1st International Conference on Performance Evaluation Methodolgies and Tools, ACM, 2006： 34.
［11］Li Q H. Research of train tracking based on HTCPN in zone controller. Chengdu： Xinan Jiaotong University, 2014.
［12］Lü J F. Modeling research of train tracking in zone system with UML. Beijing： China Railway Academy, 2012.
［13］Kang R W. The research on modeling methods and verification of Chinese train control system level 3 based on timed automata. Beijing： Beijing Jiaotong University, 2013.
［14］Olderog E R, Dierks H. Real-time systems. Cambridge： Cambridge University Press, 2008.
［15］Hessel A, Larsen K G, Mikucionis M, et al. Testing real-time system using UPPAAL. In： Formal Methods and Testing, Berlin： Springer, 2008： 77-117.
基于UML顺序图与UPPAAL的列车追踪模块建模研究
陈永刚1， 杨璐1， 王栋2
（1. 兰州交通大学 自动化与电气工程学院， 甘肃 兰州 730070； 2. 兰州交通大学 机电工程学院， 甘肃 兰州 730070）
摘要： 区域控制器(zone controller, ZC)是一个实时复杂系统， 它要求过程控制的准确性。 列车追踪场景是城市轨道交通(communication based train control, CBTC)系统中ZC的一个重要功能。 在对系统进行深层次的开发设计过程中需要对系统进行建模、 仿真和验证， 发现系统设计缺陷， 以保证系统的安全性。 通过分析ZC系统结构及列车追踪分界点处理过程， 给出满足系统安全性的功能要求和性能要求， 并采用统一建模语言(unified modeling language, UML)与时间自动机相结合的方式建立列车追踪场景中列车筛选和列车追踪分界点的时间自动机网络模型。 同时， 应用UPPAAL验证工具对系统进行仿真模拟， 验证了系统的功能和性能要求。 结果表明， 列车追踪分界点功能满足系统安全性和受限活性的规范要求。 因此， 此种建模方法是可行的， 可以将其应用于列控系统其他场景的建模与验证过程中。
关键词： 列车追踪； CBTC系统； 区域控制器； 时间自动机； UPPAAL
引用格式：CHEN Yong-gang， YANG Lu， WANG Dong. Modeling research of train tracing based on UML sequence diagram and UPPAAL. Journal of Measurement Science and Instrumentation, 2019, 10（2）： 157-167. ［doi： 10.3969／j.issn.1674-8042.2019.02.008］
[full text view]
