面向车车通信的安全计算机时间约束性分析验证

doi:10.11959/j.issn.1000?436x.2018275

通信学报 ›› 2018, Vol. 39 ›› Issue (12): 82-90.doi: 10.11959/j.issn.1000?436x.2018275

面向车车通信的安全计算机时间约束性分析验证

高莺¹,曹源²(),孙永奎³,马连川²,洪春华³,张玉琢³

¹ 中国铁道科学研究院研究生部，北京 100081
² 北京交通大学轨道交通运行控制系统国家工程研究中心，北京 100044
³ 北京交通大学电子信息工程学院，北京 100044

修回日期:2018-11-29 出版日期:2018-12-01 发布日期:2019-01-21
作者简介:高莺（1985?），女，山东烟台人，中国铁道科学研究院博士生、工程师，主要研究方向为安全分析。|曹源（1982?），男，回族，河南开封人，博士，北京交通大学副教授、博士生导师，主要研究方向为通信的列车控制技术。|孙永奎（1993?），男，河南商丘人，北京交通大学博士生，主要研究方向为铁路信号系统故障诊断。|马连川（1970?），男，河北唐山人，北京交通大学副教授，主要研究方向为列控系统安全计算机技术。|洪春华（1990?），男，福建福州人，北京交通大学硕士生，主要研究方向为列控系统安全计算机技术及形式化验证。|张玉琢（1990?），男，河南信阳人，北京交通大学博士生，主要研究方向为 Petri 网理论及在列车运行控制系统的应用。
基金资助:
国家重点研发计划基金资助项目(No.2018YFB1201601);国家自然科学基金资助项目(No.U1534208);国家自然科学基金资助项目(No.U1734211)

Analysis and verification of safety computer time constraints for train-to-train communications

Ying GAO¹,Yuan CAO²(),Yongkui SUN³,Lianchuan MA²,Chunhua HONG³,Yuzhuo ZHANG³

¹ Graduate Department, China Academy of Railway Sciences, Beijing 100081, China
² National Engineering Research Center of Rail Transportation Operation and Control System, Beijing Jiaotong University, Beijing 100044, China
³ School of Electronic and Information Engineering, Beijing Jiaotong University, Beijing 100044, China

Revised:2018-11-29 Online:2018-12-01 Published:2019-01-21
Supported by:
The National Key Research and Development Program of China(No.2018YFB1201601);The National Natural Science Foundation of China(No.U1534208);The National Natural Science Foundation of China(No.U1734211)

摘要/Abstract

摘要：

为适应基于通信的列车运行控制（CBTC, communication based train control）系统从车地模式向车车通信模式发展的趋势，针对多周期性应用并发的车载安全计算机的时间约束性，提出了基于时间 Petri 网的安全计算机时间约束性验证方法。以车载2乘2取2安全计算机为例，通过分析安全计算机多周期应用的并发性质，采用时间Petri网（TPN, time Petri net）推算其时间可调度区间，并在此基础上进行实例分析。分析和验证结果表明，在单核主频1GHz的条件下，车载安全计算机能满足3个以上周期性安全关键应用的时间约束性，表明TPN在验证和评估安全计算机中周期性应用的时间约束性方面的有效性。

关键词: 时间Petri网, 车车通信, 安全计算机, 时间约束

Abstract:

In order to adapt to the development trend of the communication based train control (CBTC) system from train-ground communication mode to train-to-train communication mode, a verification approach for time constraints of multi-period applications concurrence on-board safety computer based on time Petri net was proposed. By taking the double 2 out of 2 on-board safety computer as an example, the multi-period applications concurrence nature of the safety computer was analyzed. Time Petri net (TPN) was utilized to calculate the time schedulable interval. Then several cases were analyzed based on the inference of this approach. The analysis and verification results indicate that onboard safety computer can meet the time constraints of more than three periodic safety-critical applications under the condition of single-core with main frequency of 1GHz, which demonstrates the effectiveness of verifying and evaluating the time constraints of safety computer periodic applications using TPN.

Key words: time Petri net, train-to-train communication, safety computer, time constraint

中图分类号:

U285.49

高莺,曹源,孙永奎,马连川,洪春华,张玉琢. 面向车车通信的安全计算机时间约束性分析验证[J]. 通信学报, 2018, 39(12): 82-90.

Ying GAO,Yuan CAO,Yongkui SUN,Lianchuan MA,Chunhua HONG,Yuzhuo ZHANG. Analysis and verification of safety computer time constraints for train-to-train communications[J]. Journal on Communications, 2018, 39(12): 82-90.

图/表 11

图1

图2

图3

图4

图5

表1

图6

图7

图8

图9

图10

参考文献 17

[1]	郑升，曹源，张玉琢，等. 通用型列控系统的安全计算机设计与验证[J]. 北京交通大学学报， 2014,38(3): 128-134.
	ZHENG S , CAO Y , ZHANG Y Z , et al. Design and verification of general train control system's safety computer[J]. Journal of Beijing Jiaotong University, 2014,38(3): 128-134.
[2]	徐纪康 . 基于车车通信的新型 CBTC 系统分析[J]. 铁道通信信号， 2014,50(6): 78-80.
	XU J K . Analysis of a new CBTC system based on train-train communication[J]. Railway Signalling & Communication, 2014,50(6): 78-80.
[3]	梁靓，曹源，马连川，等. 安全计算机通信管理机制的形式化验证与实现[J]. 通信学报， 2016,37(11): 196-202.
	LIANG L , CAO Y , MA L C , et al. Formal verification and implementation of safety computer communication management mechanism[J]. Journal on Communications, 2016,37(11): 196-202.
[4]	白晓颖，汪明，陆皓，等. 实时系统时间约束验证[J]. 清华大学学报(自然科学版), 2012,52(9): 1286-1292.
	BAI X Y , WANG M , LU H , et al. Verifying timing constraints in real-time systems[J]. Journal of Tsinghua University, 2012,52(9): 1286-1292.
[5]	TSAI J J P , YANG S J , CHANG Y H . Timing constraint Petri nets and their application to schedulability analysis of real-time system specifications[J]. IEEE Transactions on Software Engineering, 1995,21(1):32-49.
[6]	XU D X , HE X D , DENG Y . Compositional schedulability analysis of real-time systems using time Petri nets[J]. IEEE Transactions on Software Engineering, 2002,28(10):984-996.
[7]	SINGH L K , RAJPUT H . Dependability analysis of safety critical real-time systems by using Petri nets[J]. IEEE Transactions on Control Systems Technology, 2017,26(2):415-426.
[8]	BASILE F , CABASINO M P , SEATZU C . Diagnosability analysis of labeled time Petri net systems[J]. IEEE Transactions on Automatic Control, 2017,62(3):1384-1396.
[9]	宋巍，窦万春，刘茜萍 . 时间约束Petri网及其可调度性分析与验证[J]. 软件学报， 2007,18(1): 11-21.
	SONG W , DOU W C , LIU X P . Timing constraint Petri nets and their schedulability analysis and verification[J]. Journal of Software, 2007,18(1): 11-21.
[10]	宋玉银，褚秀萍，蔡复之 . 基于时间Petri网的实时并行设计过程建模研究[J]. 计算机集成制造系统， 1999,5(6): 17-22.
	SONG Y Y , CHU X P , CAI F Z . Research of the process modeling of real-time concurrent design based on time Petri net[J]. Computer Integrated Manufacturing Systems, 1999,5(6): 17-22.
[11]	叶阳东，杜彦华，高军伟，等. 时间Petri网的时间知识推理算法及在铁路智能运输系统中的应用[J]. 铁道学报， 2002,24(5): 5-10.
	YE Y D , DU Y H , GAO J W , et al. A temporal knowledge reasoning algorithm using time Petri nets and its applications in railway itelligent transportation system[J]. Journal of the China Railway Society, 2002,24(5): 5-10.
[12]	叶阳东，王娟，贾利民 . 基于模糊时间Petri网的列车运行时间不确定性问题的处理[J]. 铁道学报， 2005,27(1): 6-13.
	YE Y D , WANG J , JIA L M . Processing of temporal uncertainty of train operation based on fuzzy time Petri nets[J]. Journal of the China Railway Society, 2005,27(1): 6-13.
[13]	CAO Y , MA W G , MA L C . Local fractional functional method for solving diffusion equations on cantor sets[J]. Abstract and Applied Analysis, 2014:1-6.
[14]	CAO Y , MA L C , MA W G . Mobile target tracking based on hybrid open-loop monocular vision motion control strategy[J]. Discrete Dynamics in Nature and Society, 2015:1-10.
[15]	HYYTI? E , AALTO S . On Round-Robin routing with FCFS and LCFS scheduling[J]. Performance Evaluation, 2016,97:83-103.
[16]	CAO Y , MA L C , XIAO S , et al. et al[J]. Chinese Journal of Electronics, 2017,26(5):1057-1063.
[17]	朱力，宁滨 . 基于IEEE 802.11g标准的CBTC车地通信系统设计[J]. 中国铁道科学， 2010,31(5): 119-124.
	ZHU L , NING B . The design of the CBTC train-ground communication system based on IEEE 802.11g standard[J]. China Railway Science, 2010,31(5): 119-124.

变迁	含义
t₀	发送同步确认信息至容错安全管理域
t₁	输入数据2取2逻辑对比
t₂	发送输入数据对比结果
t₃	执行系统应用逻辑阶段
t₄	应用逻辑运算结束状态汇报给容错安全管理域
t₅	输出数据2取2逻辑对比
t₆	发送输出数据对比结果

面向车车通信的安全计算机时间约束性分析验证

Analysis and verification of safety computer time constraints for train-to-train communications

在线阅读

PDF下载

可视化

摘要/Abstract

引用本文

使用本文

图/表 11

参考文献 17

相关文章 1

Metrics

推荐阅读 0