系统工程与电子技术 ›› 2020, Vol. 42 ›› Issue (2): 480-488.doi: 10.3969/j.issn.1001-506X.2020.02.30

• 可靠性 • 上一篇    下一篇

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

乔森1,2(), 黄志球1,2(), 王金永1,2(), 宛伟健1,2()   

  1. 1. 南京航空航天大学计算机科学与技术学院, 江苏 南京 211106
    2. 南京航空航天大学高安全系统的软件开发与验证技术工业和信息化部重点实验室, 江苏 南京 211106
  • 收稿日期:2019-05-13 出版日期:2020-02-01 发布日期:2020-01-23
  • 作者简介:乔森(1995-),男,硕士研究生,主要研究方向为随机混成系统、系统安全性分析、形式化方法。E-mail:15895909168@163.com|黄志球(1965-),男,教授,博士研究生导师,博士,主要研究方向为软件工程、形式化方法和云计算。E-mail: zqhuang@nuaa.edu.cn|王金永(1983-),男,博士研究生,主要研究方向为无人系统的需求建模与可靠性分析。E-mail: jinyongw@nuaa.edu.cn|宛伟健(1995-)男,硕士研究生,主要研究方向为系统安全性与可靠性分析、安全关键嵌入式系统。E-mail:wanweijianxs@163.com
  • 基金资助:
    国家自然科学基金(61772270);国家重点研发计划(2016YFB1000802)

DFT quantitative analysis method based on statistical model checking

Sen QIAO1,2(), Zhiqiu HUANG1,2(), Jinyong WANG1,2(), Weijian WAN1,2()   

  1. 1. College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing 211106, China
    2. Key Laboratory of Safety-Critical Software of Ministry of Industry and Information Technology, Nanjing University of Aeronautics and Astronautics, Nanjing 211106, China
  • Received:2019-05-13 Online:2020-02-01 Published:2020-01-23
  • Supported by:
    国家自然科学基金(61772270);国家重点研发计划(2016YFB1000802)

摘要:

动态故障树(dynamic fault tree, DFT)是对系统进行安全性分析的重要手段,基于马尔可夫链的DFT求解方法存在3个难题:一是仅可分析故障概率为指数分布的系统;二是无法分析共因失效情况;三是可能导致状态空间爆炸。因此提出一种基于统计模型检测的DFT定量分析方法。首先将DFT分解为动态逻辑门、基本构件、共因失效关系、门门和门构件间的逻辑关系;其次将动态逻辑门、基本构件和共因失效关系基于随机混成自动机形式化规约;然后通过逻辑关系重构自动机,形成随机混成自动机网络;最后通过分析一个具有共因失效关系的服从多失效概率分布的飞机结冰探测系统,表明所提方法的有效性。

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

Abstract:

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. (ⅰ) It can only analyze the system whose fault probability is exponentially distributed. (ⅱ) It is unable to resolve system common cause failure. (ⅲ) 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.

Key words: stochastic hybrid automaton, statistical model checking, stochastic system, dynamic fault tree (DFT), safety analysis

中图分类号: