铁路信号联锁逻辑形式化建模研究

铁路车站信号联锁逻辑的形式化描述无论对计算机联锁软件的开发，还是对联锁软件的测试都是非常重要的。 铁路大站的联锁逻辑十分复杂，对其进行形式化描述是一项艰难的工作。目前，国内外尚无这方面详细研究的文章和报道。本文利用层次结构的概念，采用层次化有色Petri网，以建立铁路车站信号计算机联锁软件第三方测试的现场仿真环境为目的，以车站联锁设备的层次化有色Petri网模型为背景，介绍了铁路车站信号联锁逻辑的形式化描述的基本方法。     

基于UML建模的计算机联锁进路模块Petri网验证

对于铁路车站计算机联锁软件中的重要部分之一的进路模块，使用UML对其进行建模。针对UML没有精确语义、缺少模型分析和验证手段不足的缺点，利用具有严格理论分析方法的Petri网对模型进行形式化验证，保证模型的精确性和安全性。     

基于Prover的联锁软件形式化验证过程研究

计算机联锁系统是铁路信号控制系统的核心设备,是有着苛刻安全要求的复杂控制系统。本文采用Prover形式化开发工具对联锁软件安全需求进行形式化验证。通过模型检验的形式化验证方法,遍历系统输入变量的所有状态空间.验证联锁特定应用满足系统安全需求,确保系统的安全性得以正确实现。在保证系统安全性的基础上,以全状态空间查找反例的检验方法进一步提升产品的质量。     

基于Event-B的联锁进路控制建模验证方法研究

计算机联锁系统具有典型的安全苛求特性.传统的联锁软件开发方法难以完整准确地定义需求,单纯依靠测试也无法发现软件中的所有错误,使软件在功能完整性和安全性方面难以得到保证.本文利用形式化Event-B方法和相关工具对联锁系统的核心功能-进路控制的相关功能需求和安全需求进行了建模、精化和验证,对开发高安全苛求和高可靠性的联锁软件提供了新的方法借鉴.     

形式化方法应用于计算机联锁软件的安全验证研究

铁路信号系统中的联锁系统对安全性要求极高，仅通过普通的功能测试无法保障其安全性。采用形式化验证的方式可以验证联锁系统的应用逻辑与安全需求的一致性。将通用安全需求结合具体的站场图进行实例化，得到具体的安全需求后输入带归纳功能的布尔可满足问题（SAT）约束求解器进行验证，通过覆盖所有的实例、所有周期以及每个周期所有的状态空间，保证了验证方法的完备性。     

基于Event-B的计算机联锁安全规范描述与验证

本文结合具体的站场实例,基于Event-B方法对信号开放、道岔控制、进路解锁等联锁系统关键安全规范进行了形式化模型描述和验证分析,给出了严格的分析结果.工作表明,铁路信号联锁系统是具有复杂时序逻辑的控制系统,Event-B方法适合于该类系统的描述与验证.通过形式化的联锁安全规范描述与验证,可以在系统开发的早期及时发现设计错误或漏洞,有助于提高计算机联锁系统的软件开发质量.     

基于CPN的联锁系统选岔网络建模及验证

在详细分析联锁系统选岔电路的前提下,抽象出选岔网络的联锁逻辑条件,并采用有色Petri网(Colored Petri Net,CPN)为其建立形式化验证模型,同时采用CPN TOOLS对所建立的模型进行仿真及状态空间分析,结果表明所建立的模型能够很好的描述选岔网络的工作状态。     

面向形式化验证的联锁翻译器软件设计

根据联锁系统的形式化验证系统需求,设计一种联锁数据翻译器软件的总体方案,实现站点接口文件、TLE文件和布尔逻辑文件等文件的翻译转换,生成形式化验证所需要的LCF文件.最后详细说明翻译器软件基于函数式语言OCaml的代码实现.     

基于Petri网的全自动无人驾驶列车停站场景形式化建模与验证

为进一步提高全自动无人驾驶系统的安全性,采用Petri网理论在全生命周期早期对系统运营场景的实现流程进行形式化建模与验证。选取正线运营中的列车停站这一典型运营场景,进行对象提取与状态分析,结合各对象与库所、变迁的对应关系,建立Petri网模型,并利用仿真软件PIPE对其有效性和正确性进行形式化验证。针对可能出现的异常情况对模型进行优化,设置车门与站台门开关时序,避免乘客拥挤时出现安全隐患。试验结果表明：建立的Petri网模型有界、安全且无死锁,满足列车停站场景功能需求,模型的可靠性和有效性得以验证,为全自动无人驾驶系统的开发应用与安全分析提供理论支撑。     

基于SCADE的城轨联锁软件开发方法的研究

CBTC的计算机联锁(CBI)系统是一个复杂且安全性要求非常高的系统,若按照传统的方法进行开发,很难达到其所需要的安全性和可靠性.本文提出基于高安全性应用程序开发环境(SCADE)开发城轨联锁系统软件的方法,能有效解决上述问题.文章主要介绍基于SCADE开发CBI软件的流程,建模方法,形式化验证和代码自动生成的方法.