一种状态事件故障树的定量分析方法

doi:10.3969/j.issn.0372-2112.2013.08.005

电子学报 ›› 2013, Vol. 41 ›› Issue (8): 1480-1486.DOI: 10.3969/j.issn.0372-2112.2013.08.005

一种状态事件故障树的定量分析方法

徐丙凤¹, 黄志球¹, 胡军^1,2, 魏欧¹, 肖芳雄^1,3

1. 南京航空航天大学计算机科学与技术学院, 江苏南京 210016;
2. 南京大学计算机软件新技术国家重点实验室, 江苏南京 210093;
3. 广西财经学院信息与统计学院, 广西南宁 530003

收稿日期:2012-11-19 修回日期:2013-01-17 出版日期:2013-08-25
- 通讯作者:
- 胡军
- 作者简介:
- 徐丙凤 女,1986年生于安徽安庆市.现为南京航空航天大学计算机科学与技术学院在读博士生.研究方向为软件工程,软件安全性分析与验证. E-mail:xubingfeng@nuaa.edu.cn 黄志球 男,1965年生于江苏南京人.在国防科学技术大学获工学学士和工学硕士学位,现为南京航空航天大学教授,博士生导师.主要研究方向为软件工程,服务计算,形式化方法,嵌入式软件分析与验证.
- 基金资助:
- 江苏省研究生培养创新工程 (No.CXZZ11_0218); 中央高校基本科研业务费专项资金 (No.CXZZ11_0218,No.NS2012129); 国家自然科学基金 (No.61272083,No.61170043,No.61100034,No.61262002); 回国留学人员科研启动基金 (2012)

A Method for Quantitative Analysis of State/Event Fault Tree

XU Bing-feng¹, HUANG Zhi-qiu¹, HU Jun^1,2, WEI Ou¹, XIAO Fang-xiong^1,3

1. College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing, Jiangsu 210016, China;
2. State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing, Jiangsu 210093, China;
3. School of Information and Statistics, Guangxi University of Finance and Economics, Nanning, Guangxi 530003, China

Received:2012-11-19 Revised:2013-01-17 Online:2013-08-25 Published:2013-08-25
- Supported by:
- Postgraduate Research & Practice Innovation Program of Jiangsu Province (No.CXZZ11_0218); Fundamental Research Funds for the Central Universities (No.CXZZ11_0218, No.NS2012129); National Natural Science Foundation of China (No.61272083, No.61170043, No.61100034, No.61262002); Research Fund for Returning Overseas Students (2012)

摘要/Abstract

摘要： 状态事件故障树是一种适合于描述复杂系统中失效因果链的建模技术,对系统失效结果的概率特性进行定量分析是获得系统安全性参数的一种重要途径.由于状态事件故障树是半形式化模型,需先精确描述其语义才能进行定量分析.为此,本文提出一种基于交互马尔可夫链的状态事件故障树定量分析方法.首先,通过将交互马尔可夫链的交互动作精化为输入和输出动作,提出接口交互马尔可夫链模型用于状态事件故障树的形式语义描述.然后,在此形式语义的基础上设计了一种状态事件故障树定量分析方法.最后给出了一个飞机起落架收放系统的状态事件故障树建模及概率特性定量分析的实例研究.

关键词: 安全性分析, 状态事件故障树, 交互马尔可夫链, 定量分析, 形式化方法

Abstract: State/Event Fault Tree (SEFT) is a modeling technique for describing the causal chains which lead to failure in complex systems.One important way for capturing the safety parameters of systems is quantitatively analyzing the probabilistic characteristic of system failures.As lack of precise semantics,SEFT can only be quantitatively analyzed after its semantics being precisely described.In this paper,we present a quantitative analysis method of SEFT based on Interactive Markov Chain (IMC).Firstly,Interface Interactive Markov Chain (Interface-IMC) is proposed based on refining the interactive action of IMC into input and output actions.Secondly,the precise semantics of SEFT is described based on Interface-IMC.Thirdly,a quantitative analysis method is presented based on formal semantic model of SEFT.Finally,the method in this paper is illustrated by modeling and quantitatively analyzing SEFT of aircraft landing gear system.

Key words: safety analysis, state/event fault tree, interactive Markov chain, quantitative analysis, formal method

中图分类号:

TP311

徐丙凤, 黄志球, 胡军, 等. 一种状态事件故障树的定量分析方法[J]. 电子学报, 2013, 41(8): 1480-1486.

XU Bing-feng, HUANG Zhi-qiu, HU Jun, et al. A Method for Quantitative Analysis of State/Event Fault Tree[J]. Acta Electronica Sinica, 2013, 41(8): 1480-1486.

参考文献

[1] 陈火旺,王戟,董威.高可信软件工程技术[J].电子学报,2003,31(12A):1933-1938. Chen Huo-wang,Wang Ji,Dong Wei.High confidence software engineering technologies[J].Acta Electronica Sinica,2003,31(12A):1933-1938.(in Chinese)
[2] Mahmood S,Lai R,Soo Kim Y,et al.A survey of component based system quality assurance and assessment[J].Information and Software Technology,2005,47(10):693-707.
[3] Reay KA,Andrews JD.A fault tree analysis strategy using binary decision diagrams[J].Reliability Engineering & System Safety,2002,78(1):45-56.
[4] Čepin M,Mavko B.A dynamic fault tree[J].Reliability Engineering & System Safety,2002,75(1):83-91.
[5] Kaiser B.State Event trees:A safety and reliabiity analysis techniqure for software controlled systems[D].Kaiserslautern:Universität Kaiserslautern,2007.
[6] Bryant R E.Graph-based algorithms for Boolean function manipulation[J].IEEE Transactions on Computers,1986,100(8):677-691.
[7] Hersmans H.Interactive Markov Chains[M].Berlin:Springer-Verlag,2002.57-88.
[8] De Alfaro L,Henzinger T A.Interface automata[A].Proceedings of the Joint 8th European Software Engineering Conference and 9th ACM SIGSOFT International Symposium on the Foundations of Software Engineering (ESEC/FSE 01)[C].New York:ACM Press,2001,109-120.
[9] 周颖,郑国梁,李宣东.面向模型检验的UML状态机语义[J].电子学报,2003,31(12A):2091-2095. Zhou Ying,Zheng Guo-liang,Li Xuan-dong.An operational semantics for UML state machines in model checking context[J].Acta Electronica Sinica,2003,31(12A):2091-2095.(in Chinese)
[10] Baier C,Haverkort B,Hermanns H,et al.Model-checking algorithms for continuous-time Markov chains[J].IEEE Transactions on Software Engineering,2003,29(6):524-541.
[11] Katoen JP,Khattri M,Zapreevt I.A Markov reward model checker[A].Proceedings of the Second International Conference on the Quantitative Evaluation of Systems (QEST'05)[C].Torino:IEEE Computer Society,2005.243-244.
[12] 张广泉,戎玫,朱雪阳,何亚丽,石慧娟.基于XYZ/ADL的Web服务组合描述与验证[J].电子学报,2011,39(3A):86-93. Zhang Guang-quan,Rong Mei,Zhu Xue-ya,He Ya-li,Shi Hui-juan.Specification and verification of web service composition based on XYZ/ADL[J].Acta Electronica Sinica,2011,39(3A):86-93.(in Chinese)
[13] 张君华,黄志球,曹子宁.模型检测基于概率时间自动机的反例产生研究[J].计算机研究与发展,2008,45(10):1638-1645. Zhang Jun-hua,Huang Zhi-qiu,Cao Zi-ning.Counterexample generation for probabilistic timed automata model checking[J].Journal of Computer Research and Development,2008,45(10):1638-1645.(in Chinese)
[14] Boudali H,Crouzen P,Stoelinga M.A rigorous,compositional,and extensible framework for dynamic fault tree analysis[J].IEEE Transactions on Dependable and Secure Computing,2010,7(2):128-143.

一种状态事件故障树的定量分析方法

A Method for Quantitative Analysis of State/Event Fault Tree

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 14

编辑推荐

Metrics

[1]	赵耿, 马英杰, 陈磊, 董有恒, 侯艳丽. 基于扰动时空混沌系统的动态S盒设计[J]. 电子学报, 2022, 50(8): 2037-2042.
[2]	胡文文, 周日贵. 基于d维单个量子态的半量子密钥分发方案[J]. 电子学报, 2022, 50(5): 1025-1032.
[3]	郑秋华, 胡程楠, 崔婷婷, 申延召, 曾英佩, 吴铤. 一种基于概率分析的DHR模型安全性分析方法[J]. 电子学报, 2021, 49(8): 1586-1598.
[4]	欧庆于, 罗芳, 吴晓平, 杨鹏. 基于电压毛刺故障扰动的分组密码安全性度量方法研究[J]. 电子学报, 2021, 49(3): 417-423.
[5]	宋云. 基于GHZ态局域测量的量子秘密共享[J]. 电子学报, 2019, 47(7): 1443-1448.
[6]	刘旋, 杨鹏, 董永强. 双结构网络内容共享能力研究[J]. 电子学报, 2018, 46(4): 849-855.
[7]	吴涛, 景晓军. 一种强不可伪造无证书签名方案的密码学分析与改进[J]. 电子学报, 2018, 46(3): 602-606.
[8]	房丙午, 黄志球, 王勇, 李勇. 基于混合贝叶斯网络的混合系统安全性分析方法[J]. 电子学报, 2017, 45(12): 2896-2902.
[9]	房丙午, 黄志球, 李勇, 王勇. 基于贝叶斯网络的复杂系统动态故障树定量分析方法[J]. 电子学报, 2016, 44(5): 1234-1239.
[10]	古春生, 景征骏, 于志敏, 吴访升. 基于遍历矩阵的公钥加密方案的安全性分析[J]. 电子学报, 2014, 42(10): 2081-2085.
[11]	李鹏飞;;马恒太;侯玉文;;邱田;. 移动代理完整性协议形式化分析方法研究[J]. 电子学报, 2009, 37(8): 1669-1674.
[12]	张弩云, 李军国, 黄罡, 梅宏, 叶萌, 陈滢. 一种互操作协议性能评估方法[J]. 电子学报, 2006, 34(S1): 2355-2359.
[13]	许春香;董庆宽;肖国镇. 矢量空间秘密共享-多重签名方案[J]. 电子学报, 2003, 31(1): 54-58.
[14]	林闯, 李雅娟, 王忠民. 性能评价形式化方法的现状和发展[J]. 电子学报, 2002, 30(S1): 1917-1922.