论文部分内容阅读
随着计算机、通信和控制技术的深度融合以及通信技术的飞速发展,通信在铁路信号、航空航天等这些安全苛求的控制领域中起到越来越重要的作用。对高速铁路列车运行控制系统这类安全完整性等级要求极高、且具有大量安全相关通信传输需求的安全苛求控制系统,把安全相关的通信功能独立出来不但可使系统的结构优化、性能提升、有利于系统的研发,更有利于系统的安全性验证工作。而对高铁列控系统这类硬件集成度与软件规模都空前复杂的安全苛求控制系统,采用基于严格数学定义的形式化方法能有效弥补传统性能验证方法的不足。作者在深入分析高铁列控系统的安全苛求性能需求与安全相关通信需求的基础上,成功地实施了一种适用于CTCS-3级列控系统地面设备的计算机安全相关信息通信系统的研发;并从安全苛求通信系统的角度,首次将形式化方法引入高铁列控计算机通信系统的研发工作中,采用可修复动态故障树(RDFTA)方法对系统的多模冗余结构进行了安全性验证、采用有色Petri网(CPN)方法对其安全通信协议进行了安全性验证。论文主要工作如下:1.对应用于安全苛求控制系统领域的形式化方法进行了综述,并针对适用于CTCS-3级列控系统地面设备的安全苛求通信系统的设计方案,分析选取了适用的建模与验证方法:RDFTA方法与CPN方法。2.针对安全苛求通信系统的特点,深入分析了系统的安全苛求与安全相关通信的需求,实施了一种应用于C3列控系统地面设备-临时限速服务器TSRS的安全苛求通信系统TSRS-安全通信机(TSRS-SCM)的设计方案,研制了具有安全结构的系统软、硬件平台,实现了该系统安全相关通信的功能。3.针对TSRS-SCM的多模冗余的安全结构,提出了一种基于修复盒(RB)的可修复动态故障树(RDFT)的建模与分析方法,给出了RB的形式化语义,并采用RDFTA的方法对SCM系统结构及设备上的相关功能平台进行整体建模与安全性分析,得出设备整体的顶事件概率,验证系统安全性。4.针对TSRS-SCM的安全相关通信功能,采用CPN的方法对中国铁路信号安全通信协议RSSP-II进行建模与验证,重点分析了适配及冗余管理层(ALE)与安全应用中间子层(SAI)的部分功能,通过大量仿真得出的结论验证了协议的安全性。