论文部分内容阅读
对于一旦出现异常就有可能造成生命财产损失或环境破坏的安全苛求系统来说,安全是永恒的主题,采用科学、系统的安全分析方法对系统危险进行辨识、控制、跟踪是这一类系统的设计开发不可缺少的环节。进入21世纪后计算机系统正朝着深度融合计算、通信和控制技术,形成可控、可信的网络化物理设备系统的方向发展,系统的复杂性、动态性和混杂性特征显著增强,已经远远超出了人类对计算机控制系统的行为特征以及设计理论的认识程度,给系统安全分析带来了极大的挑战。论文针对新一代安全苛求信息物理系统(Cyber Physical System, CPS)的特点,在深入分析了系统偏差行为的时序规律的基础上,定义了基于线性时间的失效传播时序逻辑(Failure Temporal Logic, FTL)系统。并将FTL系统引入失效传播转化符号(Failure Propagation Transformation Notation, FPTN)模型中,提出了Temporal-FPTN模型描述语言及其定性求解方法,为系统危险致因机理及演化规律的分析提供了更加准确、高效的分析方法。论文进一步研究了安全苛求CPS系统的行为、结构动态特征,提出了基于Temporal-FPTN模型的分层模块化动态安全分析(Hierarchical Component Based Dynamic Analysis, HiCBD)框架,从而有效降解了系统功能、结构的复杂性,同时也能够更好地契合系统开发生命周期的主要阶段。论文的主要创新点如下：(1)针对传统安全分析方法对偏差行为时序特性描述的不足,提出了基于线性时间概念的FTL系统,用于偏差事件的时序关系描述。在此基础上深入研究并证明了FTL公式的约简法则。(2)在传统安全分析方法FPTN模型中引入FTL系统,提出了Temporal-FPTN模型。并给出了Temporal-FPTN的高级文本描述,摆脱了模糊图形化描述对失效传播模型自动分析求解限制。(3)提出了基于零压缩二元判决图(Zero-suppressed Binary Decision Diagrams, ZBDDs)的最小割集序列迭代(Minimal Cut Sequence, MCSQ)求解算法。利用ZBDD有效压缩了割集运算所需要的存储空间,提高了MCSQ搜索迭代的收敛速度。(4)针对CPS系统功能和行为的复杂性问题,提出了一种基于Temporal-FPTN模型的分层安全分析框架——HiCBD框架,将平面Temporal-FPTN模型发展为分层模型。论文最后以典型的安全苛求CPS系统——基于通信的列车运行控制(Communication Based Train Control, CBTC)系统为应用对象,采用HiCBD方法完成了CBTC系统的安全分析,得到了系统危险致因的MCSQ,并对于CBTC系统的开发提出了安全相关建议,为CBTC系统的安全设计提供依据。