基于统计模型检测的DFT定量分析方法  

DFT quantitative analysis method based on statistical model checking

作　　者：乔森 黄志球[1,2] 王金永 宛伟健 QIAO Sen;HUANG Zhiqiu;WANG Jinyong;WAN Weijian(College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics,Nanjing 211106, China;Key Laboratory of Safety-Critical Software of Ministry of Industry and InformationTechnology, Nanjing University of Aeronautics and Astronautics, Nanjing 211106, China)

机构地区：[1]南京航空航天大学计算机科学与技术学院,江苏南京211106 [2]南京航空航天大学高安全系统的软件开发与验证技术工业和信息化部重点实验室,江苏南京211106

出　　处：《系统工程与电子技术》2020年第2期480-488,共9页Systems Engineering and Electronics

基　　金：国家自然科学基金(61772270);国家重点研发计划(2016YFB1000802)资助课题

摘　　要：动态故障树(dynamic fault tree,DFT)是对系统进行安全性分析的重要手段,基于马尔可夫链的DFT求解方法存在3个难题:一是仅可分析故障概率为指数分布的系统;二是无法分析共因失效情况;三是可能导致状态空间爆炸。因此提出一种基于统计模型检测的DFT定量分析方法。首先将DFT分解为动态逻辑门、基本构件、共因失效关系、门门和门构件间的逻辑关系;其次将动态逻辑门、基本构件和共因失效关系基于随机混成自动机形式化规约;然后通过逻辑关系重构自动机,形成随机混成自动机网络;最后通过分析一个具有共因失效关系的服从多失效概率分布的飞机结冰探测系统,表明所提方法的有效性。Dynamic fault tree(DFT)is an important means to analyze the safety of the system.There are three problems in solving the DFT based on Markov chain.(i)It can only analyze the system whose fault probability is exponentially distributed.(ii)It is unable to resolve system common cause failure.(iii)It is likely to cause the state space explosion.Therefore,this paper proposes a method of DFT quantitative analysis based on statistical model checking.Firstly,the DFT is decomposed into the dynamic logic gate,the basic component,the common cause failure relationship,and the logical relationships between gates and components.Secondly,the dynamic logic gate and the basic component are formalized based on the stochastic hybrid automaton.Thirdly,the automaton is reconstructed through the logical relationship to form a stochastic hybrid automaton network.Finally,the effectiveness of the proposed method is demonstrated by analyzing an aircraft icing detection system with multiple failure probability distributions and the common cause failure relationship.

关 键 词：随机混成自动机 统计模型检测 随机系统 动态故障树 安全性分析 

分 类 号：TB114.3[理学—概率论与数理统计]