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

doi:10.3969/j.issn.1001-506X.2020.02.30

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

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

乔森^1,²(), 黄志球^1,²(), 王金永^1,²(), 宛伟健^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 QIAO^1,²(), Zhiqiu HUANG^1,²(), Jinyong WANG^1,²(), Weijian WAN^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)

摘要/Abstract

摘要：

动态故障树(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

中图分类号:

TB114.3

乔森, 黄志球, 王金永, 宛伟健. 基于统计模型检测的DFT定量分析方法[J]. 系统工程与电子技术, 2020, 42(2): 480-488.

Sen QIAO, Zhiqiu HUANG, Jinyong WANG, Weijian WAN. DFT quantitative analysis method based on statistical model checking[J]. Systems Engineering and Electronics, 2020, 42(2): 480-488.

图/表 22

图1

图2

图3

图4

图5

图6

图7

图8

图9

图10

图11

图12

图13

图14

图15

图16

图17

图18

图19

表1

图20

表2

参考文献 22

1	黄志球, 徐丙凤, 阚双龙, 等. 嵌入式机载软件安全性分析标准、方法及工具研究综述[J]. 软件学报, 2014, 25 (2): 200- 218.
	HUANG Z Q , XU B F , KAN S L , et al. Survey on embedded software safety analysis standards, methods and tools for airborne system[J]. Journal of Software, 2014, 25 (2): 200- 218.
2	兰杰, 袁宏杰, 夏静. 基于离散时间贝叶斯网络的动态故障树分析的改良方法[J]. 系统工程与电子技术, 2018, 40 (4): 948- 953.
	LAN J , YUAN H J , XIA J . Improved method for dynamic fault tree analysis based on discrete-time Bayesian network[J]. Systems Engineering and Electronics, 2018, 40 (4): 948- 953.
3	房丙午, 黄志球, 王勇, 等. 基于混合贝叶斯网络的混合系统安全性分析方法[J]. 电子学报, 2017, 45 (12): 2896- 2902. doi: 10.3969/j.issn.0372-2112.2017.12.010
	FANG B W , HUANG Z Q , WANG Y , et al. A novel safety analysis method of hybrid system on hybrid Bayesian network[J]. Acta Electronica Sinica, 2017, 45 (12): 2896- 2902. doi: 10.3969/j.issn.0372-2112.2017.12.010
4	XING L , MORRISSETTE B A , DUGAN J B . Combinatorial reliability analysis of imperfect coverage systems subject to functional dependence[J]. IEEE Trans.on Reliability, 2014, 63 (1): 367- 382. doi: 10.1109/TR.2014.2299431
5	VAURIO J K . Common-cause failure models, data, quantification[J]. IEEE Trans.on Reliability, 1999, 48 (3): 213- 214. doi: 10.1109/TR.1999.799842
6	王家序, 周青华, 肖科, 等. 不完全共因失效系统动态故障树模型分析方法[J]. 系统工程与电子技术, 2012, 34 (5): 1062- 1067. doi: 10.3969/j.issn.1001-506X.2012.05.37
	WANG J X , ZHOU Q H , XIAO K , et al. Dynamic fault tree model analysis of systems subjected to incomplete common-cause failure[J]. Systems Engineering and Electronics, 2012, 34 (5): 1062- 1067. doi: 10.3969/j.issn.1001-506X.2012.05.37
7	ANAND A, SOMANI A K. Hierarchical analysis of fault trees with dependencies, using decomposition[C]//Proc.of the IEEE Reliability & Maintainability Symposium, 1998: 69-75.
8	BOUDALI H, CROUZEN P, STOELINGA M. Dynamic fault tree analysis using input/output interactive Markov chains[C]//Proc.of the 37th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, 2007: 708-717.
9	AMMAR M, HOQUE K A, MOHAMED O A. Formal analysis of fault tree using probabilistic model checking: a solar array case study[C]// Proc.of the IEEE Systems Conference, 2016: 1-6.
10	ZIO E , PODOFILLINI L , LEVITIN G . Estimation of the importance measures of multi-state elements by Monte Carlo simulation[J]. Reliability Engineering & System Safety, 2004, 86 (3): 191- 204.
11	YUGE T , YANAGI S . Dynamic fault tree analysis using Bayesian networks and sequence probabilities[J]. IEICE Trans.on Fundamentals of Electronics Communications & Computer Sciences, 2013, E96.A (5): 953- 962.
12	凌牧, 袁海文, 马钊, 等. 改进的动态故障树转化为二元决策图的成分组合算法与应用[J]. 系统工程与电子技术, 2016, 38 (7): 1600- 1605.
	LING M , YUAN H W , MA Z , et al. Enhanced component connection method and application for conversion of fault trees to binary decision diagrams[J]. Systems Engineering and Electronics, 2016, 38 (7): 1600- 1605.
13	LAPLANTE S , LASSAIGNE R , MAGNIEZ F , et al. Probabilistic abstraction for model checking: an approach based on property testing[J]. ACM Trans.on Computational Logic, 2007.
14	LEGAY A, DELAHAYE B, BENSALEM S. Statistical model checking: an overview[C]//Proc.of the International Conference on Runtime Verification, 2010: 131-146.
15	JOÃO M, ANDRÉ P, JOÃO L. Statistical model checking for distributed probabilistic-control hybrid automata with smart grid applications[C]//Proc.of the 13th International Conference on Formal Engineering Methods, 2011: 131-146.
16	ALEXANDRE D , DU D H , LARSEN K G , et al. Statistical model checking for stochastic hybrid systems[J]. Electronic Proceedings in Theoretical Computer Science, 2012, 92, 122- 136. doi: 10.4204/EPTCS.92.9
17	JENSEN P G, LARSEN K G, LEGAY A, et al. Integrating tools: co-simulation in UPPAAL using FMI-FMU[C]//Proc.of the 22nd International Conference on Engineering of Complex Computer Systems, 2017: 11-19.
18	KANG E Y, MU D, HUANG L, et al. Verification and validation of a cyber-physical system in the automotive domain[C]//Proc.of the IEEE International Conference on Software Quality, 2017: 326-333.
19	LIU W, MAO X, PU G, et al.Combining syntactic and semantic encoding for LTL bounded model checking[C]//Proc.of the Theoretical Aspects of Software Engineering Conference, 2014: 82-89.
20	JOËL O, WORRELL J. Some recent results in metric temporal logic[C]//Proc.of the International Conference on Formal Modeling and Analysis of Timed Systems, 2008: 1-13.
21	LU Y, MILLER A A, HOFFMANN R, et al. Towards the automated verification of Weibull distributions for system failure rates[C]//Proc.of the International Workshop on Formal Methods for Industrial Critical Systems and Automated Verification of Critical Systems, 2016: 81-96.
22	王小辉, 车程, 瑚洋, 等. 基于故障树的飞机结冰探测系统安全性分析[J]. 航空工程进展, 2018, 34 (2): 133- 139.
	WANG X H , CHE C , HU Y , et al. Safety analysis of aircraft icing detection system based on fault tree[J]. Advances in Aeronautical Science and Engineering, 2018, 34 (2): 133- 139.

基本事件	故障原因	故障概率分布	故障概率
X8	电源故障	均匀分布	1.0E-05
X9	ICE-IN失效	威布尔分布	(t; 0.448 2, 12 526)
X10	控制开关失效	威布尔分布	(t; 0.560 0, 4 003)
X11	SDAC1失效	指数分布	2.7E-04
X12	SDAC2失效	指数分布	2.7E-04
X13	ID硬线1失效	指数分布	1.21E-04
X14	ID硬线2失效	指数分布	1.21E-04
X15	ID左总线失效	指数分布	9.7E-04
X16	ID右总线失效	指数分布	9.7E-04
X17	FWC1失效	指数分布	3.36E-04
X18	FWC2失效	指数分布	3.36E-04

WMTL性质列表	验证结果
Pr[ < =10](<>PAND.Fail)	[9.129 65e-008, 2.009 13e-005]
Pr[ < =50](<>PAND.Fail)	[0.000 212 897, 0.000 412 897]
Pr[ < =100](<>PAND.Fail)	[0.001 543 73, 0.001 743 73]
Pr[ < =200](<>PAND.Fail)	[0.006 165 13, 0.006 365 13]

[1]	李耀华, 高源. 基于STPA-ANP模型的民机系统安全性分析[J]. 系统工程与电子技术, 2022, 44(9): 2986-2994.
[2]	陈志聪, 康锐, 祖天培, 张清源. 基于技术成熟度的确信可靠性分配方法[J]. 系统工程与电子技术, 2022, 44(1): 327-337.
[3]	柯宇航, 李艳军, 曹愈远, 张兴成. 基于模型的飞控系统安全性分析研究[J]. 系统工程与电子技术, 2021, 43(11): 3259-3265.
[4]	杨占刚, 郝雯超, 隋政, 刘建英. 基于最小割序集的独立电力系统可靠性分析[J]. 系统工程与电子技术, 2020, 42(8): 1865-1872.
[5]	赵长啸, 李浩, 董磊, 王鹏. 基于STPA-Bayes模型的机载平视显示系统安全性分析与评价[J]. 系统工程与电子技术, 2020, 42(5): 1083-1092.
[6]	陈露, 焦健, 魏钱锌. 面向模型检查的NuSMV统一建模方法[J]. 系统工程与电子技术, 2018, 40(7): 1654-1659.
[7]	兰杰, 袁宏杰, 夏静. 基于离散时间贝叶斯网络的动态故障树分析的改良方法[J]. 系统工程与电子技术, 2018, 40(4): 948-953.
[8]	凌牧, 袁海文, 马钊, 黄操. 改进的动态故障树转化为二元决策图的成分组合算法与应用[J]. 系统工程与电子技术, 2016, 38(7): 1600-1605.
[9]	尹艳玲1, 王泰华1, 曾旗2. 基于2D模型的网络系统迭代学习控制设计方法[J]. 系统工程与电子技术, 2015, 37(5): 1157-1162.
[10]	王家序，周青华，肖科，秦毅，黄彦彦. 不完全共因失效系统动态故障树模型分析方法[J]. Journal of Systems Engineering and Electronics, 2012, 34(5): 1062-1067.
[11]	姜江，李璇，陈英武，杨克巍. 证据网络及其在航天系统安全性分析中的应用[J]. Journal of Systems Engineering and Electronics, 2011, 33(6): 1270-1275.
[12]	高文华,邓飞其,张瑞秋. 凸多面体不确定随机时滞系统的非脆弱鲁棒镇定[J]. Journal of Systems Engineering and Electronics, 2011, 33(1): 146-0150.
[13]	陈淼，王道波，王志胜. 不确定随机跳变时滞系统非脆弱H_∞滤[J]. Journal of Systems Engineering and Electronics, 2010, 32(5): 1019-1023.
[14]	李玉梅1,2，关新平2，罗小元2. 线性不确定随机系统时滞相关的H_∞滤波[J]. Journal of Systems Engineering and Electronics, 2010, 32(1): 152-157.
[15]	王洪强, 方洋旺, 尹洪武. 一种随机滑模变结构制导律的设计[J]. Journal of Systems Engineering and Electronics, 2009, 31(10): 2445-2449.

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

DFT quantitative analysis method based on statistical model checking

RichHTML

PDF (PC)

可视化

摘要/Abstract

引用本文

使用本文

图/表 22

参考文献 22

相关文章 15

编辑推荐

Metrics

本文评价