论文部分内容阅读
随着计算机技术的迅速发展,嵌入式系统,尤其是嵌入式动态系统在航空、航天、医疗等安全关键领域得到了广泛的运用。如何保障嵌入式动态系统的安全性和可靠性成为当下计算机领域学术界和工业界关注的重要课题之一。动态故障树分析是一种有效的安全性分析方法,目前被广泛应用在动态系统的可靠性分析中。动态故障树通过引入动态逻辑门来弥补了传统静态故障树无法描述动态系统中时序逻辑关系的缺点。然而,动态故障树缺少精确的语义,这就导致了动态故障树的传统构建过程不可靠,建模过程中潜在的问题难以发现,从而可能导致后续的分析错误。另一方面,由于动态故障树具有复杂的动态特性,现有针对动态故障树的定量分析方法要求分析人员具有较高的专业知识能力,并且需要消耗较大的人力劳动,同时也降低了结果的精度,因此迫切需要一种具备实用工具支撑的动态故障树定量分析方法。针对以上问题,本文首先提出一种基于构件的动态故障树构建方法,并通过一种形式化语言(DFT-AC)对动态故障树进行规约和约简;其次给出一种基于概率模型检测的动态故障树定量分析方法,不仅保证了动态故障树构建过程的可靠性,同时也确保了动态故障树定量分析的精度,减少了大量的人力,并使其具备了实用工具的支撑。论文的主要研究内容如下:(1)通过系统分析,扩充了一种基于构件的系统建模方法,使其能够支持动态系统的建模,并在系统模型的基础上给出了一种动态故障树自动生成方法。(2)对AC进行了扩展,给出了一种针对动态故障树形式化规约的语言——DFT-AC,对动态故障树进行规约和约简,去除与定量分析无关的内容,保留了故障树的逻辑结构和概率属性,为后续进行定量分析建立了概率模型。(3)提出一种将动态故障树转换为PRISM代码的转换方法,能够将形式化描述的动态故障树转为支持概率模型检测的PRISM代码;并给出动态故障树定量分析属性和利用PRISM工具对动态故障树进行定量分析的过程。最后,运用本文提出的方法设计实现了动态故障树转PRISM代码的转换工具DFT2PRISM,并通过对生命保障消防系统进行案例分析,进一步说明了本方法的有效性和可行性,为嵌入式动态系统安全性分析工作提供了一种新思路。