CTCS-1级列控系统等级转换场景建模与验证

随着CTCS-1级列控系统关键技术研究工作的开展,必然要面临装载CTCS-1级车载设备的列车跨线运营至CTCS-0级线路的问题,而系统等级转换的顺利进行是实现列车安全跨线运营的基础。通过系统功能分析,建立了系统多分辨率功能模型,以识别等级转换场景需求;根据场景需求,结合现行系统规范,完善了CTCS-1级系统等级转换场景的方案;采用基于UML的NuSMV建模与验证方法,建立了等级转换场景的UML模型和NuSMV模型,并验证了场景模型的活性、确定性等属性,从而证明了完善后的场景方案满足场景需求,且符合系统规范。文中对CTCS-1级系统等级转换场景的探讨可为相关规范的修订提供支持。     

基于CPN的等级转换场景建模分析

针对正常情况下CTCS-2级列控系统和CTCS-3级列控系统之间的等级转换,探讨了一种基于有色Petri网模型的系统建模方法。模型中引入非周期消息模型,模拟在GSM-R网络中RBC（无线闭塞中心,Radio Block Centre）与车载设备之间消息的传送过程,并建立基于有色Petri网的等级转换控车场景模型,讨论在不同消息重发时间间隔、不同列车速度对等级转换场景完成成功率的影响。验证了该建模方法的有效性,说明了影响等级转换成功率的因素。     

基于CPN的列控系统等级转换建模与分析

在高速列车运行过程中,列控系统等级转换过程所用的时长和转换成功概率,直接影响列车运行安全和行车效率。利用有色Petri网对CTCS-3级列控系统和CTCS-2级列控系统之间等级转换以及典型设备故障导致降级场景分别建模,模拟等级转换过程中RBC（Radio Block Center,无线闭塞中心）,车载设备,有源应答器之间的信息交互过程。分析了列车速度对等级转换实时性的要求和对转换成功概率的影响,以及突发降级的可能性,结果表明建模方法满足CTCS-3级列控系统的安全性和兼容性要求。     

基于UML与有色Petri网的RBC切换场景的建模方法研究

针对仅有一台车载电台正常的RBC(无线闭塞中心)切换场景,探讨了一种基于UML模型和有色Petri网(CPN)的系统建模方法;首先利用UML模型的顺序图及状态图描述RBC切换流程和过程中车载设备的状态转移,再从UML状态图中提取信息构造相应的有色Petri网模型,最后利用CPN Tools的状态空间工具分析模型的有界性、家态性、活性和公平性,得到的模型动态行为符合RBC切换功能的要求;论文验证了该建模方法的有效性,为完善RBC系统设计提供依据。     

CTCS-3列控系统RBC切换的形式化建模、分析与验证

针对影响RBC切换质量的列车速度、RBC切换时间等诸因素,以及澄清对RBC交接协议安全性在认识上的一些误区,利用随机Petri网形式化描述工具,建立了CTCS-3列控系统RBC切换模型.通过理论分析和仿真实验,验证了不同速度条件下高速列车越区运行RBC交接协议A、B的可靠性、安全性和合理性.交接协议B作为协议A的冗余措施,由于考虑了RBC切换过程中通信中断时间,从RBC切换成功概率上讲,并不存在安全上的问题,但降低了RBC切换效率,对行车效率有所影响;列车速度进一步提高时,RBC切换的可靠性下降,可考虑适当增加RBC重叠覆盖区域、场强和列车间隔时间裕量.     

CTCS-3列控系统RBC切换的形式化建模、分析与验证

针对影响RBC切换质量的列车速度、RBC切换时间等诸因素, 以及澄清对RBC交接协议安全性在认识上的一些误区, 利用随机Petri网形式化描述工具, 建立了CTCS-3列控系统RBC切换模型。通过理论分析和仿真实验, 验证了不同速度条件下高速列车越区运行RBC交接协议A、B的可靠性、安全性和合理性。交接协议B作为协议A的冗余措施, 由于考虑了RBC切换过程中通信中断时间, 从RBC切换成功概率上讲, 并不存在安全上的问题, 但降低了RBC切换效率, 对行车效率有所影响; 列车速度进一步提高时, RBC切换的可靠性下降, 可考虑适当增加RBC重叠覆盖区域、场强和列车间隔时间裕量。     

CTCS-2级列控系统的形式化建模与验证

由于 CTCS-2级列控系统设计复杂,因此提出一种将统一建模语言(UML)与符号模型检验相结合的形式化建模与验证方法。分析CTCS-2级列控车载设备的模式转换场景,对其进行UML建模得到UML类图和状态图,制定转换规则对UML模型进行扩展和抽象,使其转化为NuSMV模型。将待验证的系统性质和转化后的检验程序输入符号模型检验系统进行验证,验证结果都为true,表明CTCS-2级列控车载设备的模式转化场景具有活性、可达性和安全性。     

基于灰色系统理论高速列车ATO速度控制器研究

速度控制器是ATO系统的核心单元,也是列控系统的重要组成部分,针对目前高速列车无ATO功能的情况,研究智能的ATO系统速度控制器对实现高速列车自动驾驶具有的重要意义。通过分析CTCS-3级列控系统的结构和功能,提出了在CTCS-3级列控系统中增加ATO系统速度控制器的方案。首先设计了速度控制器与车载及地面设备的连接方式,实现了信息交互;而后应用灰色系统理论善于研究外延明确内涵不清系统的特点,建立速度控制器模型,进行预测及决策计算,得到比较合理的列车自动驾驶控制策略;最后采用遗传算法对其进行优化,得到最优控制策略。仿真结果表明,该方法实现了高速列车在CTCS-3级列控系统下的自动驾驶,列车运行的各项性能都得到了提高。     

光电干扰武器系统C3I可执行建模的研究

UML已经成为面向对象分析与设计建模事实上的标准。基于UML的C3I系统模型的设计结果是对系统的静态表述,而C3I系统的本质是动态的。着色Petri网(CPN)具有强大的描述能力及严密的数学基础和多种分析手段,并且是可以仿真运行的。提出了从UML产品映射到可用于逻辑、行为和性能方面体系结构评价的CPN可执行模型的方法,对光电干扰武器系统C3I进行了UML建模的一般描述,阐述了光电干扰武器系统C3I从UML产品映射到CPN建立可执行模型的过程。通过对可执行模型CPN的仿真可对光电干扰武器系统C3I进行完整准确的评价。     

城市轨道交通CBTC自动控制系统及设计实践研究

为提高城市轨道交通CBTC自动控制系统的实时性,基于铁路数字移动通信系统(GSM-R)的列控通信系统,构建GSM-R首层模型、GSM-R下行链路模型和GSM-R信道模型,保证了列控数据传输的可靠性,降低了列控数据传输时延。最后,利用CPN Tools工具进行仿真。结果表明,所提基于GSM-R的列控通信系统模型,可完成数据帧在城市轨道交通列车与车站之间的传输与差错处理,实现了城市轨道交通CBTC的自动控制。相较于基于LTE-R的列控通信系统模型,所提模型最高运行速度提高了10 km/h,运行时间缩短了7 s,具有更好的实时性和追踪效率,能高效灵活地调整城市轨道交通列车的运行状态,且不容易受到信道质量的影响,为提高城市轨道交通CBTC自动控制系统的实时性提供了参考。     

Hybrid MARTE statecharts

The specification of modeling and analysis of real-time and embedded systems (MARTE) is an extension of the unified modeling language (UML) in the domain of real-time and embedded systems. Even though MARTE time model offers a support to describe both discrete and dense clocks, the biggest effort has been put so far on the specification and analysis of discrete MARTE models. To address hybrid real-time and embedded systems, we propose to extend statecharts using both MARTE and the theory of hybrid automata. We call this extension hybrid MARTE statecharts. It provides an improvement over the hybrid automata in that: the logical time variables and the chronometric time variables are unified. The formal syntax and semantics of hybrid MARTE statecharts are given based on labeled transition systems and live transition systems. As a case study, we model the behavior of a train control system with hybrid MARTE statecharts to demonstrate the benefit.     

一种基于扩展I*框架和UML的面向Agent需求建模方法

以分布式电子商务系统为研究背景，提出了一种基于扩展I^*建模框架和UML的面向Agent需求建模方法．该方法将需求工程划分为早期需求获取和后期需求规格说明两个阶段：在早期需求获取阶段，在I^*策略模型中引入服务依赖概念，用于描述组织背景中Agent的意图和Agent之间的依赖关系，同时描述系统内部Agent和分布式环境中其他Agent之间的依赖关系；在后期需求规格说明阶段，采用扩展的UML在Agent抽象层次上建立统一的需求模型．该方法还为早期需求获取平滑过渡到后期需求规格说明提供了统一的模型映射规则．从而保持模型的一致性．     

模糊时间Petri网及扩展的模糊时间Petri网

网络实时系统对时间和QoS有严格要求,因此对设计、实现和测试的技术和工具都有很高的要求。模糊时间Petri网是将模糊集合理论用于不确定的或主观的时间信息的表示,在每个变迁上添加时间间隔约束对模糊时间Petri网进行扩展得到扩展的模糊时间Petri网,它是一种对网络实时系统进行建模和分析的形式化模型,Petri网数学理论基础能保证并发系统的可靠性和正确性。本文详细地介绍了模糊时间Petri网及可扩展的时间Petri网,可扩展的时间Petri网的网精简方法,使用design／CPN仿真,及使用EFTN对多媒体同步建模,并探讨了进一步研究的方向。     

实时软件系统开发技术

分析了开发实时系统和实时软件系统的特殊性，讨论了传统实时软件系统开发技术(包括RTSA技术、DARTS技术、JSD技术、NRL方法、OOA＆OOD技术等)，并比较了它们各自的优缺点．详细讨论了面向对象技术在实时软件系统开发中的应用，对统一建模语言(UML)在实时软件系统中的应用也进行了深入分析和讨论．在分析了实时UML(UML-RT)的不足之后，提出了融合UML和CPN的实时软件开发技术，并用一个实例说明了如何利用该技术进行实时软件开发．