LIN Junting1， XU Qian1， CHEN Yong2
（1. School of Automation and Electrical Engineering， Lanzhou Jiaotong University， Lanzhou 730070, China；
2. School of Electronic and Information Engineering， Lanzhou Jiaotong University， Lanzhou 730070， China）
Abstract： The short-range wireless communication technology has advanced considerably and provides the feasibility of train-train (T2T) communication link in the communication-based train control system. The introduction of the T2T link would reduce the headway and improve operational efficiency. Formal methods are system design techniques that use rigorously specified mathematical models to ensure all behaviors work as expected. And it is exactly the functional safety verification needed. Therefore, to deal with the functional safety verification of the T2T link, an untimed colored petri net model is first constructed. Secondly, the verification process is performed. Conclusions can be drawn from the state space report and the computation tree logic queries. Lastly, the model is parameterized, and then data log files are obtained for further performance measurement. Results show that the proposed criteria are satisfied and there are no defects in the basic design requirements. The transmission delay has considered the reconnection, transmission errors and the interruption. The probability of the delay lower than 150 ms accounts for 98.106%, which meets the specification and the previous field test.
Key words： functional safety； formal methods； colored Petri net (CPN)； state space analysis； performance measurement
References
［1］Lehner A, Rico Garcia C, Strang T, et al. Measurement and analysis of the direct train to train propagation channel in the 70 cm UHF-band. Lecture Notes in Computer Science, 2011: 45-57.
［2］Su K L. Research on access technology for D2D communication mode under emergency scenarios of high-speed railway. Beijing: Beijing Jiaotong University, 2016.
［3］Wang X X, Liu L J, Tang T, et al. Enhancing communication-based train control systems through train-to-train communications. IEEE Transactions on Intelligent Transportation System, 2019, 20(4): 1544-1561.
［4］Zhang Y, Wang H F. Topological manifold-based monitoring method for train-centric virtual coupling control systems. IET Intelligent Transport Systems, 2020, 142(2): 91-102.
［5］David B. Alstom’s simplified CBTC technology to debut in Lille. International Railway Journal, 2013, 53(6): 29-30.
［6］Zhu L, Yao D Y, Zhao H L. Reliability analysis of next-generation CBTC data communication systems. IEEE Transactions on Vehicular Technology, 2019, 68(3): 2024-2034.
［7］Shan D H. Performance assessment of train-train communication with high-speed railway based on stochastic network calculus. Chengdu: Southwest Jiaotong university, 2018.
［8］Chen M S, Bao Y X, Sun H Y, et al. Survey on formal method of trustworthy construction for communication-based train control systems. Journal of Software, 2017, 28(5): 1183-1203.
［9］Kurt J, Lars M K. Coloured Petri Nets: Modelling and Validation of Concurrent Systems, Berlin, Springer, 2009.
［10］Wu D H, Schnieder E. Scenario-based system design with colored Petri nets: an application to train control system. Software and Systems Modeling, 2018, 17: 295-317.
［11］Chen L J, Tang T, Zhao X Q, et al. Verification of the safety communication protocol in train control system using colored Petri net. Reliability Engineering and System Safety, 2012, 100: 8-18.
［12］Xu T H, Zhao H L, Tang T. Colored Petri nets based reliability analysis of ETCS train radio communication. Journal of the China Railway Society, 2008, 1: 38-42.
［13］Wang R, Zheng W, Liang C, et.al. An integrated hazard identification method based on the hierarchical Colored Petri Net. Safety Science, 2016, 88: 166-179
［14］Liu H D, Su M, Peng H Q, et.al. Braking performances of urban rail trains. Journal of Transportation Systems Engineering and Information Technology, 2011, 11(6): 93-97.
［15］China Associate of Metros. CZJS/T 0069.Technical equipment professional committee of China Association of Metros. LTE-M interface specification for CBTC: China Railway Publishing House, Beijing, 2016.
［16］Teng C M. Study on the application of device-to-device communication in train operation control system. Beijing: Beijing Jiaotong University, 2017.
［17］Jiang H L, Zhao H L, Zhu L, et al. Field test of urban rail transit train-wayside communication-based 5.9 GHz TD-LTE. Journal of the China Railway Society, 2016, 38(5): 53-59.
车车通信链路的功能安全性验证及性能测试
林俊亭1， 徐倩1， 陈永2
（1. 兰州交通大学 自动化与电气工程学院， 甘肃 兰州 730070；2. 兰州交通大学 电子信息工程学院， 甘肃 兰州 730070）
摘要:短程无线通信技术快速发展， 为基于通信的列车控制系统中的列车到列车 （Train to train, T2T） 通信链路提供了可行性。 引入T2T链路将缩短追踪间隔、 提高运营效率。 形式化方法是一种系统设计技术， 使用有严格数学定义的模型来确保所有行为按预期发生， 而这正是所需的功能安全性验证。 为了进行T2T通信链路的功能安全性验证， 首先， 建立了非赋时有色Petri网（Colored Petri net, CPN）模型。 其次， 执行验证过程， 并从状态空间报告和计算树逻辑语句中得出结论。 最后， 模型参数化， 并获得数据日志文件以进行性能测试。 结果表明， 满足所提出的准则， T2T链路的基本设计要求没有缺陷。 传输时延计算中考虑了重连、 传输错误、 中断情况。 端到端时延小于150 ms的概率为98.106%， 符合规范及现场测试结果。
关键词:功能安全性； 形式化方法； 有色Petri网； 状态空间分析； 性能测试
引用格式：LIN Junting, XU Qian, CHEN Yong. Functional safety verification and performance measurement of train-train communication link. Journal of Measurement Science and Instrumentation, 2021, 12（4）： 463-471. DOI： 10.3969／j.issn.1674-8042.2021.04.010
[full text view]
