基于MSC与UPPAAL的列控系统等级转换场景形式化验证

等级转换是C3级列控系统的重要场景,是列控系统兼容性的集中体现,转换的成功与否直接关系到列车的运行安全和行车效率。因此,有必要对设计规范中所描述的转换过程进行形式化建模和验证,以保障系统的安全性和实时性。为保证设计规范与所建模型的一致性,采取消息顺序图(MSC)与时间自动机相结合的方式,建立等级转换场景中C2级向C3级转换过程的MSC模型,并将其转换为时间自动机模型。应用UPPAAL对模型的安全性和受限活性进行仿真验证,结果表明设计规范中所描述的转换过程是安全可靠的,可以满足C3级列控系统的兼容性和安全性要求。     

基于UPPAAL的城市轨道交通CBTC区域控制子系统建模与验证

CBTC(Communication Based Train Control)系统可有效提高轨道交通的列车运营效率,降低系统建设和维护费用.在系统研发过程中需对系统进行建模、仿真和验证,发现系统设计缺陷,以保证系统的安全性.CBTC区域控制子系统是一实时控制系统,它要求控制时间的精确性和控制过程的准确性.本文通过分析城市轨道交通CBTC区域控制子系统的结构,给出满足该子系统安全性的功能和性能要求,并结合时间自动机理论方法提出包含列车、速度距离控制器、区域控制器和多车控制队列的时间自动机网络模型.同时,应用UPPAAL验证工具对CBTC区域控制子系统进行仿真建模,并验证该子系统功能和性能要求,从而保证了系统模型的安全性和受限活性.     

CBTC区域控制器切换场景的建模与验证

区域控制器(Zone Controller,ZC)通过与联锁系统(Computer Interlocking,CI)、车载控制器(Vehicle On Board Controller,VOBC)和列车自动监督系统(Automatic Train Supervision,ATS)等其他子系统信息交互来为列车计算移动授权,是基于通信的列车运行控制系统(Communication Based Train Control,CBTC)重要的地面安全设备。研究区域控制器的功能需求,构建满足边界切换实时性、安全性特点的模型有助于保证列车在线路上高效、安全的运行。在现有建模方式的基础上,采用统一建模语言(Unified Modeling Language,UML)和层次时间有色Petri网(Hierarchical Timed Colored Petri Net,HTCPN)相结合的方法对ZC边界切换场景下的区域控制器和车载子系统之间的信息交互过程进行分析。从车载VOBC状态变化的角度构建用于验证切换场景安全性的UML模型和HTCPN模型,并以CPN Tools作为仿真平台对其进行验证。根据CPN ...     

客运专线CTCS-3级列控系统无线闭塞中心的建模与验证

本文分析客运专线CTCS-3级列控系统中无线闭塞中心(RBC)子系统软件的功能和性能约束,在此基础上采用时间自动机理论进行RBC子系统形式化语义描述,建立TER-QSR时间自动机网络模型,并应用UPPAAL验证工具对RBC子系统进行仿真分析,验证RBC的安全性(Safety)和受限活性(Bounded Liveness),同时进行RBC切换时间的优化。     

基于MSC与UPPAAL的高铁跨界临时限速建模与验证

临时限速服务器是高铁列控系统的重要组成部分,其不仅要校验CTC下发的临时限速命令,还要与相邻调度台临时限速服务器之间进行频繁的信息交互,因此对其安全性和实时性要求也更苛刻。为了满足高铁列控系统对其运行的要求,采用时间自动机理论和消息顺序图(MSC)相结合的方法,首先建立跨界临时限速命令的MSC模型和时间自动机子模型,再利用UPPAAL验证工具对形式化语法BNF描述的时间自动机子模型属性进行验证。根据仿真验证结果确认了跨界临时限速信息的安全性和受限活性,为进一步开发临时限速服务器功能提供了重要的依据。     

基于Timed-UML顺序图的RBC交接形式化建模与分析

在CTCS-3级列控系统中,采用RBC技术将线路划分成多个管辖区段。当列车行驶并跨越相邻RBC交界区域时,控制权将会移交至前方相邻RBC,整个过程称为RBC交接。在运行中,RBC交接过程能否实时安全可靠地执行,直接影响着列车的行车效率和乘客的生命安全。采用一种基于添加实时约束的UML顺序图与时间自动机结合的模型来建立RBC交接场景。以双车载电台的RBC切换策略出发,建立切换的Timed-UML顺序图模型,然后按照UML-TA转换规则,建立得到完整的时间自动机网络模型。并利用UPPAAL验证工具对RBC交接模型进行形式化建模及分析,对模型的死锁和功能实现做了验证,从而达到对CTCS-3级RBC子系统的实时性以及设计规范合理性的验证目的。     

高速铁路CTC分界口临时限速系统建模与验证

临时限速是高速铁路列控系统的重要组部分,CTC行车调度台分界口处的临时限迷信息交互频繁,对实时性的要求也更苛刻.为满足其实时性要求,采用时间自动机理论,结合分界口处临时限速相邻设备间的交互过程,分别建立各设备的时间自动机模型,通过时间自动机的积构建整个交互系统的网络模型,并利用UPPAAL验证工具对模型的功能和性能属性进行形式化验证.验证结果确认了交互过程中系统的安全性和受限活性.     

高速铁路列控系统运营场景实时性的建模与验证

高速铁路列控系统是一个典型的分布式实时系统,其时间约束主要反映在运营场景中子系统之间的交互过程中。时序逻辑的扩展方法并不能完全满足描述分布式实时系统性质的需要,并且随着系统的复杂性提高,列控系统运营场景中诸如超时、期限、直到…才等形式化描述与验证上存在不足。本文提出一种适合于列控系统场景建模与验证的方法,其核心思想是使用混合通信顺序进程HCSP(Hybrid Communicating Sequential Process)形式化描述分布式实时系统模型,提出转换规则,转换成时间自动机网络模型并进行自动验证。最后通过对典型场景无线闭塞中心RBC(Radio Block Center)切换的相关属性进行建模与验证,分析证明方法的有效性。     

基于UPPAAL的列车自动防护系统形式化建模与验证

本文分析列车自动防护(ATP)系统的结构和功能需求,建立系统的时间自动机模型,采用UPPAAL模型验证工具对模型的活性和安全性进行验证.结果表明,采用时间自动机对安全苛求实时系统进行建模与验证,可以有效地保证系统的可靠性和实时性.     

一种基于场景的CTCS-3列车控制系统建模方法研究

对CTCS-3列车控制系统进行有效的测试、分析和验证是保证列车运行安全和旅客生命财产安全的重要手段,而形式化模型是系统测试、分析和验证的基础。本文以CTCS-3列车运行控制系统的UML非形式化模型为基础,以自动机模型作为系统形式化模型描述的数学工具,研究UML顺序图(场景)自动转化为自动机网模型的方法。首先将场景的UML顺序图自动转化为子系统的子自动机模型,然后通过合并不同场景的子自动机模型,得到子系统的组元自动机模型,最后通过对通信通道的建模得到系统的自动机网模型。使用本方法,基于系统的UML顺序图模型可以自动生成系统的自动机网模型。     

基于时间自动机的CBI道岔转换时间建模与验证

针对CBTC计算机联锁安全性十分重要的问题，介绍时间自动机理论，分析CBTC计算机联锁系统的结构和与传统联锁系统的区别，以CBTC联锁系统的道岔转换功能为例，采用UPPAAL建立了道岔转换模型，分析模型的安全需求。表明了在联锁系统开发过程中采用基于时间自动机建模与验证的方法的可行性和有效性。     

移动授权的形式化建模与验证

基于通信的列车运行控制系统(Communications-Based Train Control System,CBTC)相较于传统的基于轨道的列车运行控制系统,无论是从功能方面还是性能方面都有了很大的改进。在系统的研发过程中,对其进行建模和验证,能够发现系统设计的缺陷,进而保证系统的安全性和功能性。移动授权(Movement Authority,MA)是CBTC系统的核心功能,用来保证列车的安全运行间隔。通过对移动授权生成原理的研究,采用时间自动机和其自动验证工具UPPAAL对其进行建模以及验证,验证结果表明,搭建的移动授权模型能够达到规定的安全要求和功能要求。因此UPPAAL能够对复杂的实时系统进行仿真验证。     

基于SCADE的安全软件开发方法研究

针对传统软件开发方式已经不能满足高安全性系统安全性、完整性的需求,本文提出了基于SCADE的安全软件开发方法,分析SCADE开发的原理、流程及应用方式,并以城市轨道交通列车运行控制系统的区域控制器ZC为例,基于SCADE对ZC列车管理功能进行建模和验证。通过实例分析,证明基于SCADE的软件开发方法,可以有效保障高安全性系统的安全性和完整性,为其提供了一种新的开发方式。     

基于模型的CBTC区域控制系统安全软件开发

传统的软件开发方法不能满足基于通信的列车控制(CBTC)区域控制系统(ZC)的开发需求.结合北京地铁亦庄线研究项目,介绍一种基于模型的系统开发方法,给出ZC系统的软件容错结构,阐述该系统的移动授权和列车管理功能建模方法,并从模型覆盖率分析和形式化验证两方面深入分析系统安全性保障措施.ZC系统的研究项目表明,基于模型的开...     

Timed RAISE方法在列控系统等级转换场景中的应用研究

高速铁路列车运行控制系统是一个复杂的实时性系统,结合其实际特点,将域方法作为系统描述的切入。通过对模型检验和定理证明两种验证方法的分析比较,提出使用基于定理证明的时间化工业软件工程的严格方法Timed RAISE形式化方法对等级转换(CTCS-2级至CTCS-3级)场景进行描述,并对其场景交互一致性和实时性进行验证,结果表明该场景不会出现场景交互一致性错误,也不会违反时间的约束。     

基于TRSL的RBC等级转换场景研究

无线闭塞中心等级转换场景作为中国列车运行控制系统主要场景之一,切换成功与否直接影响高速列车的安全和运行效率。通过对形式化验证方法的分析,采用基于定理证明的时间化工业软件工程规范语言的严格方法(Timed Rigorous Approach to Industrial Software Engineering Specification Language,TRSL),在对等级转换过程进行分析的基础上,设计交互信息图,构建状态迁移图,并结合域建模方法实现对该场景的TRSL描述,最后利用语言推理规则,结合系统特性,实现对切换正确性和实时性的双重验证,结果表明:该场景满足系统规范对功能性和实时性的要求,继而说明该方法的有效性、正确性和通用性,为我国列控系统的设计开发和验证提供一种新的途径和依据。     

CTCS-3级列控系统规范的建模与形式化验证方法研究

CTCS-3级列控系统规范是CTCS-3级列控系统设计与开发的基础,是实现互联互通以及确保系统高效率与安全性的关键环节。然而,依靠经验与直觉制定的规范不可避免地存在某些漏洞或者安全隐患,因此对CTCS-3级列控系统规范进行建模与形式化验证显得十分必要。本文提出CTCS-3级列控系统规范建模与形式化验证方法,此方法的特点是能够在系统规范、模型、验证工具以及验证结果之间建立一条跟踪链,从而始终保证系统规范、模型及程序代码之间的一致性。结合笔者运用此方法对CTCS-3级列控系统规范建模与形式化验证的实践,证明这种方法是可行的、高效的。     

基于Timed RAISE的高速列车RBC切换协议形式化建模及验证

在CTCS-3(Chinese Train Control System Level 3)级列控系统中,RBC(Radio Block Center)切换是影响列车安全高效运行的重要环节,现阶段对RBC切换协议进行验证分析所使用的形式化方法还存在状态爆炸或描述性质单一等问题。基于Timed RAISE的形式化方法,结合域的模型,在对RBC切换流程分析的基础上,构建状态转移图,得到切换协议的形式化模型,使用等价和推断的推理规则对模型的正确性和实时性进行推理验证,得到的结果表明,RBC切换协议满足规范标准对正确性与实时性的要求,将验证结果与其他文献的结论进行比较分析,说明该方法具有通用性,对于推广其在列控系统场景验证中的应用有一定的实际意义。