【作者】 牛儒；

【导师】 唐涛；

【作者基本信息】 北京交通大学 ， 交通信息工程及控制， 2010， 博士

【摘要】 对于一旦出现异常就有可能造成生命财产损失或环境破坏的安全苛求系统来说,安全是永恒的主题,采用科学、系统的安全分析方法对系统危险进行辨识、控制、跟踪是这一类系统的设计开发不可缺少的环节。进入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系统的安全设计提供依据。更多还原

【Abstract】 Safety is an ever-lasting topic for safety system in which any anomaly will result in serious damage to both life and property, as well as destruction of environment. It is therefore indispensable for the design and development of the system of this type to identify, control and trace the hazard events of the system, by means of scientific and systemic safety analysis. However, computer system, since the beginning of the 21st century, tends to coordinate computation, communication and automotive technology to construct a controllable and reliable system with a network of physical equipments. Consequently, the complexity, dynamics and hybridity of the system is increasing dramatically, such that it surpasses human beings’apprehension of the behavior and the principles for the design of the controlling computer systems, and brings about a challenge for safety analysis of the system.The thesis, on the basis of the specification of the sequence rule of the deviant behavior of the system, defines the Failure Temporal Logic (FTL) for linear time, with respect to the characterization of Safety Critical Cyber Physical System (CPS). It provides the descriptive language and qualitative solution method for Temporal-FPTN model, and a more accurate and effective analysis of the motivation for the harm of the system and the generalization of the evolution of the system. Furthermore, the present study explores the dynamic feature of the behavior and the structure of CPS, and establishes a Hierarchical Component Based Dynamic Analysis Framework (hence, HiCBD), based on Temporal-FPTN model, thus decompounding the function and structure complexity of the system, accommodating the lifecycle of the system.The innovation of the thesis is as follows:(1) The study proposes a FTL system depending on linear time which is applied to the characterization of sequential relation of deviant events, and establishes a framework for the transformation of FTL into LTL, on the basis of which a reduction rule for the formula of FTL is demonstrated.(2) The study, through the addition of the FTL system into Failure Propagation Transformation Notation (hence, FPTN), offers a description of Temporal-FPTN in advanced text, effectively avoids the constraints on the automatic analysis of the Failure Propagation Model with the vague graphics description.(3) The study, based on ZBDDs, presents a resolution method for Minimum Cut Set seQuence (MCSQ). The application of ZBDD compress the storage space for the computation of cut-set, and simultaneously increases the convergence rate of the iterative search for MCSQ.(4) The study also forms a framework of Hierarchical Component Based Dynamic Analysis (hence, HiCBD) on the basis of Temporal-FPTN, transforming the Temporal-FPTN model into a hierarchical model.The thesis ends with an accomplishment of the safety analysis of a kind of typical safety-critical CPS-CBTC system by means of HiCBD. And the MCSQ of each system level hazards has been calculated. The achievements of this study prove to be a reinforcement of the design of CBTC in China.更多还原