检索结果-南通市图书馆

基于增强型BN的ctcs-1级ATP可靠性研究

维普期刊数据库

同方期刊数据库评论

在线全文

学校读者我要写书评

暂无评论

北京交通大学学报 2017年第5期41卷 58-65页

作者：刘中田徐越王昊北京交通大学电子信息工程学院北京100044

结合ctcs-2级与ctcs-3级列控系统设计和运用经验,铁路总公司提出了ctcs-1级列控系统的研制需求,该系统车载ATP设备将取代LKJ与机车信号对既有线列车的控制.本文以ctcs-1级ATP为主要研究对象,对比分析模块级冗余与系统级冗余方案下ctcs-1... 详细信息

结合ctcs-2级与ctcs-3级列控系统设计和运用经验,铁路总公司提出了ctcs-1级列控系统的研制需求,该系统车载ATP设备将取代LKJ与机车信号对既有线列车的控制.本文以ctcs-1级ATP为主要研究对象,对比分析模块级冗余与系统级冗余方案下ctcs-1级ATP系统可靠性.根据ctcs-1级列控系统总体技术方案,构建模块级冗余与系统级冗余ATP可靠性框图,建立对应增强型贝叶斯网络(BN)模型.借助增强型BN正向推理,求解两种设计方案下ATP可靠性定量指标,评估两种设计方案的优劣.利用增强型BN模型逆向推理,求解列车超速防护(ATP)设备故障下基本单元条件失效概率,查找两种冗余设计方案的潜在薄弱环节.评估结果表明:两种方案下ctcs-1级ATP RAM指标均满足需求规范要求,但采用模块级冗余设计的ctcs-1级ATP RAM指标更优;外围冷备模块条件失效率明显高于其他模块,为ctcs-1级ATP的薄弱环节.

关键词：列车运行自动化增强型BN RAM ctcs-1 ATP

ctcs-1级列控系统RDC数据生成及验证方法的研究

维普期刊数据库

同方期刊数据库评论

在线全文

学校读者我要写书评

暂无评论

CTCS-1级列控系统RDC数据生成及验证方法的研究

作者：卢铃冉北京交通大学

学位级别：硕士

中国列车运行控制系统(Chinese Train Control System,ctcs)是保障列车运行安全和效率的安全苛求系统。列控数据作为信号设备信息、列车状态信息和线路信息的载体,其正确性是列车安全运行的重要前提。目前针对不同的列控子系统,数据描... 详细信息

中国列车运行控制系统(Chinese Train Control System,ctcs)是保障列车运行安全和效率的安全苛求系统。列控数据作为信号设备信息、列车状态信息和线路信息的载体,其正确性是列车安全运行的重要前提。目前针对不同的列控子系统,数据描述方式不同且没有特定的数据规范,列控数据的验证也主要依靠人工校验和仿真测试相结合的方式,效率低且正确性难以保证。针对上述问题,本文以研究ctcs-1级列控系统地面核心设备—区域列控数据中心(RDC)的静态数据验证为例,从RDC数据组织方式设计和数据验证两个方面进行了研究,首先建立了 RDC静态数据模型,然后提出了数据验证的总体框架,设计和开发了 RDC数据自动化验证工具,实现了数据的自动化验证。论文完成的工作包括:(1)设计RDC数据组织方式,建立RDC静态数据模型。通过分析RDC系统需求将数据分为点元素、线元素和区域元素,构建各数据元素之间的逻辑关系模型,使之既体现线路拓扑关系又便于后期维护和更新,最终建立RDC静态数据结构模型,并结合实际线路数据生成RDC静态数据库。(2)提出数据建模和验证的总体框架,将其分为四个阶段:数据约束规则提取、数据验证模型建立、模型检验、数据验证工具开发。首先根据列控数据规范和RDC功能需求,结合数据编制和验证经验,将数据约束规则总结为域值关系规则、映射关系规则、关联关系规则和连续关系规则,为保证验证过程的全面性和条理性,论文设计了数据字段的横向验证和纵向验证方法,基于数据约束规则建立数据验证流程的CSP模型。(3)基于上述形式化数据验证模型,建立数据约束规则、数据验证模型、模型检验、结果分析之间的双向跟踪链,得到符合数据约束规则的RDC数据验证模型。论文从正确性、有效性、安全性三个方面对模型进行检验,首先利用ProB验证器检验模型是否存在死锁、活锁等问题以及是否满足约束规则,在此基础上通过CSP-Petri模型转换,利用Petri网可达树分析法对模型的安全性进行分析,通过多次模型修改和重验最终证明了模型满足要求。(4)基于以上数据验证模型,借助.NET Framework平台开发了 RDC数据自动化验证工具。以实际线路数据测试软件的验证效果,通过对比经软件验证无误和经传统数据验证方法证实无误的数据,说明通过自动化验证软件对RDC数据进行验证可在提高验证效率的同时保证数据的正确性,也证明了本文提出的RDC数据验证方法的可行性。

关键词：数据验证 ctcs-1 CSP 模型检验 RDC

ctcs-1级列控系统车站数据服务器SDS建模验证与实现研究

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

CTCS-1级列控系统车站数据服务器SDS建模验证与实现研究

作者：张茜北京交通大学

学位级别：硕士

C3高铁动车组利用普速线迂回运行系统(简称ctcs-1级列控系统)是为了支持高铁线路故障后动车组能够在普速线路上运行而设计的一套全新的系统,该系统在尽量减少对普速线路上既有设备改造的前提下,把普速线路上广泛使用的ctcs-0级列控系统... 详细信息

C3高铁动车组利用普速线迂回运行系统(简称ctcs-1级列控系统)是为了支持高铁线路故障后动车组能够在普速线路上运行而设计的一套全新的系统,该系统在尽量减少对普速线路上既有设备改造的前提下,把普速线路上广泛使用的ctcs-0级列控系统改造成ctcs-1级列控系统,既解决了普速线路存在的安全相关问题,又保证了动车组在普速线路上的安全高效运行。该系统的技术方案目前处在研究阶段,车站数据服务器(SDS)作为该系统地面的核心设备,将生成的无线报文通过无线广播通信方式发送给车载设备,对SDS进行建模验证与实现可以降低开发成本和开发风险,促进ctcs-1级列控系统方案的完善。论文基于SCADE完成对SDS的建模验证与实现。论文完成的主要工作如下:(1)研究基于SCADE的软件开发方法,并提出基于SCADE的SDS总体研究方案,该研究方案包括SDS功能需求分析、SDS参与的关键场景建模验证、SDS功能详细设计、SDS功能建模验证与实现等内容。(2)SDS功能需求分析。通过梳理ctcs-1级列控系统总体技术规范文档中与SDS相关的内容,分析SDS的交互功能需求和内部功能需求,把SDS的功能细化为系统自检模块、数据配置模块、动态数据管理模块、无线报文发送模块、状态监测和记录模块。在分析SDS功能需求的过程中,发现SDS与列车通信时采用无线单向广播方式,在现有的列控系统中从未使用过,所以需要从SDS参与的场景中选取无线广播通信场景进行深入研究。(3)SDS参与的关键场景——无线广播通信场景的建模验证。通过分析ctcs-1级列控系统的总体技术规范、无线广播通信场景的需求,对无线广播通信场景进行详细设计。采用Sys ML语言对场景建模,通过设计的Sys ML-PRISM模型的转换算法将其转换为PRISM模型,并在概率模型检验工具PRISM中进行模型验证,证明了场景设计的合理性以及无线单向广播通信方式的可行性,确定了场景相关的技术指标,作为后续研究的基础。(4)SDS功能建模验证与实现。依据分析的SDS的功能需求,完成SDS每个功能模块的详细设计、SCADE模型设计,结合研究无线广播通信场景时确定好的场景相关技术指标,完善建立的每个功能模块的SCADE模型,把各个功能模块集成在一起构成SDS的SCADE模型。通过SCADE仿真验证工具进行SDS的SCADE模型的仿真、覆盖率分析,验证模型的正确性和仿真的完备性。采用形式化验证方法证明所建的SDS的模型是满足安全属性的,保证了SDS的安全性。采用代码生成器KCG自动生成面向工程的C代码,把C代码放到目标机中联调联试,验证了设计的SDS模型满足预期的功能要求,以及用SCADE开发SDS系统的可行性。本文有图84幅,表14个,参考文献57篇。

关键词： ctcs-1 车站数据服务器无线广播通信场景 SysML PRISM SCADE 建模与验证

ctcs-1级列控车载功能兼容方案建模与验证

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

CTCS-1级列控车载功能兼容方案建模与验证

作者：王颖卓北京交通大学

学位级别：硕士

车载功能兼容研究主要解决的是列车跨线运行的问题,其一是通过合理的系统功能设计,使车载系统能支持列车在低等级线路条件下的安全运行控制,其二是通过合理的场景设计,使面临跨线运行的列车能安全且高效地实现在不同控制等级之间的转换... 详细信息

车载功能兼容研究主要解决的是列车跨线运行的问题,其一是通过合理的系统功能设计,使车载系统能支持列车在低等级线路条件下的安全运行控制,其二是通过合理的场景设计,使面临跨线运行的列车能安全且高效地实现在不同控制等级之间的转换。ctcs-1级列控系统总体技术方案中提出了在车载系统内部集成C0级系统功能的设想,而项目的前期工作集中于C1级系统的核心业务功能,未能对C1/C0的车载功能兼容问题给出明确方案。对此,本文总结了当前C1车载功能兼容方案中存在的问题,并对当前方案进行了优化设计。提出了针对功能兼容方案的建模与验证框架,建立了功能兼容方案的基础模型,并综合利用NuSMV符号模型检验技术和TCPN建模与仿真方法,从系统功能设计和列车运营场景两个维度,对优化后的功能兼容方案进行了验证。本文完成的主要工作如下:(1)C1车载功能兼容需求分析与方案的优化设计。梳理了 C1级列控系统规范文档中功能兼容相关内容,对核心控制单元的交互方案进行了比选,确定其一为本文的研究基础;通过系统功能分析,提取了 C1/C0车载功能兼容需求;从车载系统结构、功能单元交互等方面对现有方案进行了优化。(2)方案验证研究框架的提出与基础模型的构建。提出了基于模型的方案验证思路,从类、交互、行为三个维度给出了由方案到模型的抽象原则,结合优化后的功能兼容方案和C0核心业务逻辑,完成了对优化后功能兼容方案的完整构建,实现了方案描述的规范化与可视化。(3)车载功能兼容方案的验证。研究了基于UML的符号模型检验方法,定义了 UML到NuSMV的转换规则,建立了方案的NuSMV模型;提取了待验证的属性,并从中提炼出了相应的CTL属性表达式;根据模型的执行结果,回溯不满足属性要求的状态与变量,定位错误原因,进而对方案和模型进行修正,得到了正确、完善的兼容方案。(4)等级转换场景的验证与性能分析。从线路设计、车地通信交互等方面对C1/C0等级转换场景进行了详细设计;考虑场景过程中各子环节的主要时间约束,建立了场景的TCPN模型;分析了模型的动态性能,证明了场景设计的合理性;探讨了场景的实时性能,给出了线路设计建议。通过本文的研究,最终得到了较完善的C1车载功能兼容方案,验证结果表明,该方案满足功能兼容需求且符合C1级系统规范。相关成果可为后续C1级列控技术研究提供理论支持,文中所建立的兼容方案的基础模型也可为今后系统多维度验证与分析提供模型基础。图58幅,表8个,参考文献55篇。

关键词： ctcs-1 功能兼容建模与验证 NuSMV 等级转换场景

基于动态规划的ctcs-1级列控系统测试序列自动生成方法研究

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

基于动态规划的CTCS-1级列控系统测试序列自动生成方法研究

作者：李智北京交通大学

学位级别：硕士

中国列车运行控制系统 1 级(Chinese Train Control System level 1,简称 ctcs-1)是适用于200km/h以下新建及改造线路,采用目标距离连续速度控制模式监控列车安全运行的列控系统,目前正处于研发阶段,需要进行一系列测试以确保设备满足... 详细信息

中国列车运行控制系统 1 级(Chinese Train Control System level 1,简称 ctcs-1)是适用于200km/h以下新建及改造线路,采用目标距离连续速度控制模式监控列车安全运行的列控系统,目前正处于研发阶段,需要进行一系列测试以确保设备满足相关技术规范,因此需要编制大量的测试序列来满足测试各种需求。目前所使用的ctcs-1测试序列均由手工编写,工作量大,对编制人员的专业性要求高,效率较低。因此,有必要开展ctcs-1列控系统测试序列计算机辅助生成方法和工具的研究。北京交通大学前期已对ctcs-3级列控系统测试序列的生成方法进行了大量研究,并开发了 ctcs-3级列控系统测试序列辅助生成工具。论文在总结这些研究工作的基础上,根据ctcs-1级列控系统的特点,提出了基于动态规划的ctcs-1列控系统测试序列生成方法和基于专家系统的测试序列合理性验证方法。论文完成的主要工作如下:(1)分析了 ctcs-1测试序列生成过程中需要解决的关键问题,即测试案例的串接顺序和测试地点的选择,由此提出了基于动态规划的测试序列自动生成方法。首先,结合模式转换和测试场景对测试案例之间的距离进行评估,以案例间最短距离为优化目标,采用动态规划算法,求解得到最优的测试案例串接顺序。其次,从多个维度(轨道区段类型、是否有应答器等)对案例与测试地点的差异度进行评估,以最小差异度和作为优化目标,采用动态规划算法,求解得到最优的测试地点。最后,采用查表方式实现测试配合条件的添加。(2)提出了基于专家系统的ctcs-1测试序列合理性验证方法。首先深入研究ctcs-1级列控系统相关规范,整理相关知识,采用框架表示法描述测试过程中车载设备的状态转换过程(起始状态、结束状态等),采用产生式规则描述规则知识。其次,从测试序列中获取测试步骤、待测案例、站场结构等相关数据并整理为合理性验证过程要求的数据格式(状态转换过程)。最后采用正向推理得到每次状态转换过程的实际结束状态,采用“位与”法比较状态转换过程的实际起始/结束状态是否与期望一致,以此验证测试序列的合理性。(3)在上述测试序列自动生成方法的基础上,对ctcs-1测试序列生成工具进行整体设计和详细设计,采用Visual Studio 2013开发平台以及C#语言完成测试序列生成工具的开发。

关键词：列控系统 ctcs-1 测试序列动态规划专家系统

基于SysML和时间自动机的ctcs-1级列控系统RDC建模与验证

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

基于SysML和时间自动机的CTCS-1级列控系统RDC建模与验证

作者：王晓丹北京交通大学

学位级别：硕士

随着铁路系统的升级和发展,铁路既有线的运输效率和安全等级提升已提上议程。ctcs-1(Chinese Train Control System Level 1)级列控系统是为了改进既有线控车而设计的—套全新系统,可以极大地提升普速列车安全性、可靠性、运输效率和自... 详细信息

随着铁路系统的升级和发展,铁路既有线的运输效率和安全等级提升已提上议程。ctcs-1(Chinese Train Control System Level 1)级列控系统是为了改进既有线控车而设计的—套全新系统,可以极大地提升普速列车安全性、可靠性、运输效率和自动化水平。它实现了以低成本解决既有线存在的诸多问题,对比普速铁路现有系统有明显的优势。区域数据控制中心(Regional Data Control Center,RDC)作为ctcs-1级列控系统的核心地面设备,可以将实时生成的行车数据通过无线网络发送给列车,大大减少了列车存储的数据量,同时也减少司机对控车数据的操作,降低了人为因素带来的隐患。论文完成了 RDC系统功能模型的建立及验证,包括RDC系统与外部设备的信息交互、行车数据的生成等流程,为ctcs-1级列控系统的实际应用奠定了基础。论文完成的主要工作有:首先,通过研究ctcs-1级列控系统与RDC子系统的功能需求,包括内部功能与对外交互功能,同时总结出其特点并进行需求建模,借鉴了以往的列控系统子系统建模研究方法,确定了使用SysML建模语言和时间自动机理论来进行RDC系统的建模和验证。其次,对RDC系统的对外交互模块进行信息交互流程分析,将RDC系统交互流程分为地面设备交互模块和车载设备交互模块两个部分,RDC系统交互流程包括设备启动、列车注册、正常行车、列车注销、RDC切换,利用SysML顺序图对以上场景进行建模,通过转换算法将其转换为时间自动机网络模型后在UPPAAL中进行模型验证。然后,对RDC系统行车数据的生成进行了研究。RDC系统将对外交互模块接收到的TSRS提供的临时限速信息、CBI提供的列车进路信息、列车提供的位置信息,按照不同运营场景生成动态线路数据,包括行车路径串接与临时限速延伸。再结合自身存储的静态线路数据生成行车数据,通过无线网络发送给车载设备从而实现正常控车。利用SysML活动图对以上流程进行建模,得到RDC行车数据生成模型,转换为时间自动机网络模型后在UPPAAL中验证。最后,在建模分析的基础上,完成RDC仿真软件设计与开发。以京沪线某段的真实场景在实验室平台上进行系统联调测试,验证了 RDC功能模型的正确性与合理性。

关键词： RDC ctcs-1 SysML 时间自动机 UPPAAL

基于模型的ctcs-1级列控地面子系统仿真研究

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

基于模型的CTCS-1级列控地面子系统仿真研究

作者：桑杰北京交通大学

学位级别：硕士

地面子系统作为列控系统的重要组成部分,不仅担负着与车载设备的实时安全通信,也直接关系到列车在整个线路中的安全运行。ctcs-1级列控系统升级优化了 C0系统的缺陷和不足,兼容吸纳了 ctcs-2级、ctcs-3级列控系统的诸多优势,形成了一套... 详细信息

地面子系统作为列控系统的重要组成部分,不仅担负着与车载设备的实时安全通信,也直接关系到列车在整个线路中的安全运行。ctcs-1级列控系统升级优化了 C0系统的缺陷和不足,兼容吸纳了 ctcs-2级、ctcs-3级列控系统的诸多优势,形成了一套适用于200km/h以下新建或改造线路的过渡型列控方案。然而ctcs-1级列控系统在跨线运营方案、兼容C0功能等方面,还需要进一步深入研究;既往关于列控系统建模仿真的研究多依托于计算机编程语言来实现;采用基于模型设计方法建模仿真列控系统的研究多见于城轨列控系统仿真或大铁车载设备仿真,部分研究仅实现了各模块的独立功能,没有实现模块到模型、再到系统的综合仿真过程。本论文针对上述问题,运用基于模型的设计方法展开对ctcs-1级列控系统地面子系统的建模仿真研究。论文主要工作如下:(1)在深入分析了各设备、各控制系统的详细功能和接口关系后,基于Simulink/Stateflow建模方法,提出了适用于C1地面子系统的模型框架和建模仿真流程。(2)针对地面子系统各模块进行Simulink/Stateflow图形化建模,随后将模块连接整合,实现了地面子系统的基本逻辑功能。(3)将真实线路数据融入仿真研究,进行线路模型设计,通过MATLAB图形化显示环境监测Simulink/Stateflow模型的输出状态,将模型仿真结果准确显示于站场图中。(4)结合Simulink通用的检查工具筛查模型的配置及设计漏洞,通过输入不同的进路号、临时限速信息、列车位置信息来仿真C1列控系统典型列车运行场景,进而分析仿真结果的准确性,并给出系统中信号机模型转为C代码的示例过程。图74幅,表13个,参考文献42篇。

关键词： MBSE ctcs-1 地面子系统建模仿真 Simulink/Stateflow 邻接矩阵

基于STPA的ctcs-1级列控系统安全分析方法的研究

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

基于STPA的CTCS-1级列控系统安全分析方法的研究

作者：杨续颖北京交通大学

学位级别：硕士

ctcs-1级列控系统是为提升200km/h以下新建及改造线路安全性、可靠性、运输效率和自动化水平而对既有线列控系统进行的一次技术升级。列控系统作为典型的安全苛求系统,其安全性对整个铁路运输系统举足轻重,因此,对列控系统进行安全分析... 详细信息

ctcs-1级列控系统是为提升200km/h以下新建及改造线路安全性、可靠性、运输效率和自动化水平而对既有线列控系统进行的一次技术升级。列控系统作为典型的安全苛求系统,其安全性对整个铁路运输系统举足轻重,因此,对列控系统进行安全分析来识别特定应用场景存在的安全隐患,有着非常重要的意义。与传统的风险识别方法相比,STPA能够更系统地识别风险。但是STPA分析过程过度依靠人工,对技术人员的专家经验依赖程度高。另外由于复杂系统功能和行为的多样性,仅仅依靠人工分析难以保证结果的全面性和准确性。因此,本文基于CPN动态模型提出形式化的STPA-CPN方法来辨识系统危险致因。本文的主要研究工作如下:(1)首先,以侧线接车和临时限速场景为例,完成了 STPA的安全分析流程。在使用分层控制框图、SysML顺序图、OCL语言建立系统模型的基础上,参照STPA提供的四类引导词实现不恰当控制行为辨识,并完成控制缺陷分析,为验证本文所提方法有效性做铺垫。(2)然后,通过比较SysML和CPN两种建模方法的优缺点论证了 SysML活动图到有色Petri网模型转换的必要性和可操作性。建立侧线接车和临时限速两个场景的SysML活动图,给出活动图到CPN模型的转换规则及其简化规则,完成CPN模型的建立与化简。并运用CPN Tools工具生成两个场景CPN模型的状态空间可达图。(3)为提高本文提出的形式化安全分析方法的通用性,在编写搜索危险状态可达路径程序的基础上,于C#环境下完成了可达性分析工具Reachability Analysis Tool的开发。该工具以不安全控制行为和状态空间可达图为输入,输出为危险状态可达路径。(4)最后,根据可达性分析工具输出的危险状态可达路径,通过追溯状态迁移过程进行致因分析,改善了 STPA中依靠人工辨识容易出现遗漏和错误的问题,并且降低了对安全分析人员专家经验的依赖。并与STPA安全分析出的结果对比,结果证明将CPN可达性分析引入STPA是可行、有效的。图62幅,表5个,参考文献72篇

关键词： ctcs-1 STPA CPN 系统理论危险源识别

基于TCPN的ctcs-1级列控系统RDC形式化建模与分析

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

基于TCPN的CTCS-1级列控系统RDC形式化建模与分析

作者：徐越北京交通大学

学位级别：硕士

新一代 ctcs-1(Chinese Train Control System-Level 1)级列控系统是为提升普速列车安全性、可靠性、运输效率和自动化水平而对既有线列控系统进行的一次技术升级,目的是实现车载线路数据下放到地面,由地面统一管理的现实需求,保证临时... 详细信息

新一代 ctcs-1(Chinese Train Control System-Level 1)级列控系统是为提升普速列车安全性、可靠性、运输效率和自动化水平而对既有线列控系统进行的一次技术升级,目的是实现车载线路数据下放到地面,由地面统一管理的现实需求,保证临时限速的即时更新,减少司机对控车数据的操作,提升既有线列控设备的自动化水平。区域列控数据中心(RDC)为ctcs-1级列控系统地面设备的核心,负责ctcs-1级列车的管理,以无线形式向列车提供行包含线路数据、链接应答器、进路与临时限速的行车数据。RDC系统的形式化建模与验证分析能保证RDC系统软件的完备性,安全性,可靠性,对于既有线列控设备技术升级具有促进意义。论文选择基于ML语言的时间有色Petri网(TCPN)对RDC系统进行功能设计、建模仿真和验证分析研究,论文完成的主要工作如下:首先,综合有色Petri网与时间Petri网二者特点,提出针对实时并发系统的TCPN形式化建模与分析方法,给出了基于ML语言的TCPN模型建模与分析一般流程,在此基础上,构建了 ctcs-1级RDC建模与模型验证分析的整体框架,该框架涵盖了 RDC需求分析、功能设计、建模、功能验证分析、软件架构设计、软件开发与仿真实现等内容。然后,通过分析RDC系统特点、内部功能需求、交互功能需求,对RDC系统总体功能与主要模块功能进行设计,其中模块功能设计涵盖ctcs-1级列车注册与启动、注销、等级转换、行车数据生成、列车移交等主要运营场景,并且对比分析了 RDC与ctcs-3级无线闭塞中心(RBC)在主要运营场景中的功能差异。其次,根据设计的RDC系统功能,分别建立了 RDC交互功能与主体功能的TCPN模型,并采用时间有色Petri网分层的思想降低模型复杂度与状态空间维度,将主体功能模型细化为车载设备自检子模型、RDC工作状态检查子模型、RDC与C1-ATP建链子模型、通信会晤建立子模型、列车数据确认子模型、行车数据交互子模型;同时建立列控等级切换、列车移交、C1车与既有车追踪运行特殊场景模型,利用仿真验证工具CPN-Tools对模型仿真运行,从功能逻辑正确性、完备性、与技术规范一致性的角度进行验证分析;此外,在逻辑功能验证成功基础上,以列车移交为例进行RDC时间性能分析。最后,根据所建RDC功能模型,对系统软件进行层级架构设计与功能编码实现,在列控实验室平台上进行系统联调测试,通过“五站四区间”场景测试验证了RDC形式化功能模型的正确性与用于RDC系统软件开发的可行性。

关键词： RDC ctcs-1 时间有色Petri网形式化建模 CPN-Tools