摘要

在工业控制、航空电子、汽车行业等安全关键领域,软件构件代替机械和电子构件已经成为一种趋势。系统安全分析主要是确定引起故障的关键行为和组合,并且判断系统设计中存在的不足。AFDX网络是航空电子系统中的数据网络,具有高的可靠性、抗击恶劣环境的适应性和实时性等特点。已有的针对AFDX网络可靠性模型都是基于故障树或者动态故障树。但是,在AFDX网络中许多构件已经被软件所替代,而故障树或者动态故障树不能满足软件构件系统的复杂性和动态依赖等特性。为了进行构件化软件系统的安全性分析,Bernhard Kaiser等在故障树的基础上加入事件和状态等概念,提出了状态事件故障树建模方法。基于状态事件故障树求解其顶事件的发生概率和最小割集序列的定量和定性分析已经取得一些成果,对提高系统的安全性带来了很大帮助。本文主要围绕状态事件故障树研究其最小割集序列的定性分析和顶事件失效概率的定量分析,然后基于AFDX网络数据完整性建立状态事件故障树并做安全性分析和验证。主要工作包括以下内容:首先,由于状态事件故障树缺乏严格的形式化语义,为了解决引起顶事件失效的最小割集序列问题,先将状态事件故障树转换为确定随机Petri网,再将确定随机Petri网中的逻辑门按照一定的规则进行化简,并用库所代替构件对应的Petri网;接着改进基于Petri网的关联矩阵法,使得其适合求解最小割集序列,并开发了自动求解工具minCut。其次,针对状态事件故障树顶事件失效概率问题,给出了基于随机混成自动机的概率特性分析方法。对于含有确定时延事件的状态事件故障树,用基于Interface-IMC的方法不能分析其概率特性。因此,本文将状态事件故障树转换为随机混成自动机做概率特性分析。针对状态事件故障树中的逻辑门和构件,分别给出了它们到随机混成自动机的转换语义。然后用模型检测工具UPPAAL-SMC做概率特性分析,并且通过一个实例,与基于Interface-IMC的概率特性分析方法进行了比较。最后,分析AFDX网络中交换机和终端的结构以及数据帧传输过程,建立相应的状态事件故障树。用状态事件故障树精确的对AFDX网络中软件构件的内部失效行为建模。接着将建立好的模型转换为确定随机Petri网和随机混成自动机分别做最小割集序列和顶事件发生概率求解分析。根据AFDX网络数据完整性的定量和定性分析结果,可以优化AFDX的结构和元件。