一种状态事件故障树的定量分析方法
第８期２０１３年８月
电 子 学 报Ｖｏｌ．４１ Ｎｏ．８
一种状态事件故障树的定量分析方法
２３
徐丙凤１，黄志球１，胡 军１，，魏 欧１，肖芳雄１，（１．南京航空航天大学计算机科学与技术学院，江苏南京２１００１６；２．南京大学计算机软件新技术国家重点实验室，江苏南京２１００９３；
３．广西财经学院信息与统计学院，广西南宁５３０００３）
摘 要： 状态事件故障树是一种适合于描述复杂系统中失效因果链的建模技术，对系统失效结果的概率特性进
行定量分析是获得系统安全性参数的一种重要途径．由于状态事件故障树是半形式化模型，需先精确描述其语义才能进行定量分析．为此，本文提出一种基于交互马尔可夫链的状态事件故障树定量分析方法．首先，通过将交互马尔可夫链的交互动作精化为输入和输出动作，提出接口交互马尔可夫链模型用于状态事件故障树的形式语义描述．然后，在此形式语义的基础上设计了一种状态事件故障树定量分析方法．最后给出了一个飞机起落架收放系统的状态事件故障树建模及概率特性定量分析的实例研究．
关键词： 安全性分析；状态事件故障树；交互马尔可夫链；定量分析；形式化方法
中图分类号： ＴＰ３１１ 文献标识码： Ａ 文章编号： ０３７２－２１１２（２０１３）０８－１４８０－０７电子学报ＵＲＬ：ｈｔｔｐ：／／ｗｗｗ．ｅｊｏｕｒｎａｌ．ｏｒｇ．ｃｎ ＤＯＩ：１０．３９６９／ｊ．ｉｓｓｎ．０３７２－２１１２．２０１３．０８．００５
ＡＭｅｔｈｏｄｆｏｒＱｕａｎｔｉｔａｔｉｖｅＡｎａｌｙｓｉｓｏｆＳｔａｔｅ／ＥｖｅｎｔＦａｕｌｔＴｒｅｅ
（１．ＣｏｌｌｅｇｅｏｆＣｏｍｐｕｔｅｒＳｃｉｅｎｃｅａｎｄＴｅｃｈｎｏｌｏｇｙ，ＮａｎｊｉｎｇＵｎｉｖｅｒｓｉｔｙｏｆＡｅｒｏｎａｕｔｉｃｓａｎｄＡｓｔｒｏｎａｕｔｉｃｓ，Ｎａｎｊｉｎｇ，Ｊｉａｎｇｓｕ２１００１６，Ｃｈｉｎａ；
２．ＳｔａｔｅＫｅｙＬａｂｏｒａｔｏｒｙｆｏｒＮｏｖｅｌＳｏｆｔｗａｒｅＴｅｃｈｎｏｌｏｇｙ，ＮａｎｊｉｎｇＵｎｉｖｅｒｓｉｔｙ，Ｎａｎｊｉｎｇ，Ｊｉａｎｇｓｕ２１００９３，Ｃｈｉｎａ；３．ＳｃｈｏｏｌｏｆＩｎｆｏｒｍａｔｉｏｎａｎｄＳｔａｔｉｓｔｉｃｓ，ＧｕａｎｇｘｉＵｎｉｖｅｒｓｉｔｙｏｆＦｉｎａｎｃｅａｎｄＥｃｏｎｏｍｉｃｓ，Ｎａｎｎｉｎｇ，Ｇｕａｎｇｘｉ５３０００３，Ｃｈｉｎａ）
２３
ＸＵＢｉｎｇ－ｆｅｎｇ１，ＨＵＡＮＧＺｈｉ－ｑｉｕ１，ＨＵＪｕｎ１，，ＷＥＩＯｕ１，ＸＩＡＯＦａｎｇ－ｘｉｏｎｇ１，
Ａｂｓｔｒａｃｔ： Ｓｔａｔｅ／ＥｖｅｎｔＦａｕｌｔＴｒｅｅ（ＳＥＦＴ）ｉｓａｍｏｄｅｌｉｎｇｔｅｃｈｎｉｑｕｅｆｏｒｄｅｓｃｒｉｂｉｎｇｔｈｅｃａｕｓａｌｃｈａｉｎｓｗｈｉｃｈｌｅａｄｔｏｆａｉｌｕｒｅｉｎ
ｃｏｍｐｌｅｘｓｙｓｔｅｍｓ．Ｏｎｅｉｍｐｏｒｔａｎｔｗａｙｆｏｒｃａｐｔｕｒｉｎｇｔｈｅｓａｆｅｔｙｐａｒａｍｅｔｅｒｓｏｆｓｙｓｔｅｍｓｉｓｑｕａｎｔｉｔａｔｉｖｅｌｙａｎａｌｙｚｉｎｇｔｈｅｐｒｏｂａｂｉｌｉｓｔｉｃｃｈａｒ－ａｃｔｅｒｉｓｔｉｃｏｆｓｙｓｔｅｍｆａｉｌｕｒｅｓ．Ａｓｌａｃｋｏｆｐｒｅｃｉｓｅｓｅｍａｎｔｉｃｓ，ＳＥＦＴｃａｎｏｎｌｙｂｅｑｕａｎｔｉｔａｔｉｖｅｌｙａｎａｌｙｚｅｄａｆｔｅｒｉｔｓｓｅｍａｎｔｉｃｓｂｅｉｎｇｐｒｅｃｉｓｅ－ｌｙｄｅｓｃｒｉｂｅｄ．Ｉｎｔｈｉｓｐａｐｅｒ，ｗｅｐｒｅｓｅｎｔａｑｕａｎｔｉｔａｔｉｖｅａｎａｌｙｓｉｓｍｅｔｈｏｄｏｆＳＥＦＴｂａｓｅｄｏｎＩｎｔｅｒａｃｔｉｖｅＭａｒｋｏｖＣｈａｉｎ（ＩＭＣ）．Ｆｉｒｓｔｌｙ，Ｉｎ－ｔｅｒｆａｃｅＩｎｔｅｒａｃｔｉｖｅＭａｒｋｏｖＣｈａｉｎ（Ｉｎｔｅｒｆａｃｅ－ＩＭＣ）ｉｓｐｒｏｐｏｓｅｄｂａｓｅｄｏｎｒｅｆｉｎｉｎｇｔｈｅｉｎｔｅｒａｃｔｉｖｅａｃｔｉｏｎｏｆＩＭＣｉｎｔｏｉｎｐｕｔａｎｄｏｕｔｐｕｔａｃｔｉｏｎｓ．Ｓｅｃｏｎｄｌｙ，ｔｈｅｐｒｅｃｉｓｅｓｅｍａｎｔｉｃｓｏｆＳＥＦＴｉｓｄｅｓｃｒｉｂｅｄｂａｓｅｄｏｎＩｎｔｅｒｆａｃｅ－ＩＭＣ．Ｔｈｉｒｄｌｙ，ａｑｕａｎｔｉｔａｔｉｖｅａｎａｌｙｓｉｓｍｅｔｈｏｄｉｓｐｒｅ－ｓｅｎｔｅｄｂａｓｅｄｏｎｆｏｒｍａｌｓｅｍａｎｔｉｃｍｏｄｅｌｏｆＳＥＦＴ．Ｆｉｎａｌｌｙ，ｔｈｅｍｅｔｈｏｄｉｎｔｈｉｓｐａｐｅｒｉｓｉｌｌｕｓｔｒａｔｅｄｂｙｍｏｄｅｌｉｎｇａｎｄｑｕａｎｔｉｔａｔｉｖｅｌｙａｎａ－ｌｙｚｉｎｇＳＥＦＴｏｆａｉｒｃｒａｆｔｌａｎｄｉｎｇｇｅａｒｓｙｓｔｅｍ．
Ｋｅｙｗｏｒｄｓ： ｓａｆｅｔｙａｎａｌｙｓｉｓ；ｓｔａｔｅ／ｅｖｅｎｔｆａｕｌｔｔｒｅｅ；ｉｎｔｅｒａｃｔｉｖｅＭａｒｋｏｖｃｈａｉｎ；ｑｕａｎｔｉｔａｔｉｖｅａｎａｌｙｓｉｓ；ｆｏｒｍａｌｍｅｔｈｏｄ
１ 引言
嵌入式系统在航空、汽车以及工业控制等安全关键
领域的广泛应用使得对其进行安全性分析成为系统开
［１］
发过程中的重要部分．随着嵌入式软件系统功能和复杂度的增加，目前嵌入式系统多为组件化分布式架［２］构．为对组件化分布式架构的嵌入式系统进行安全性分析，研究人员提出了一系列相关的安全性建模分析方［３～５］法．其中，状态事件故障树（Ｓｔａｔｅ／ＥｖｅｎｔＦａｕｌｔＴｒｅｅ，
收稿日期：２０１２－１１－１９；修回日期：２０１３－０１－１７；责任编辑：蓝红杰
ＳＥＦＴ）是一种表达系统失效因果链的建模方法，顶层
事件表示失效的发生，通过逻辑门和基本构件表达失效发生的因果链．ＳＥＦＴ中包含了软件系统的行为模型，以及系统中构件的失效与系统失效结果之间的因果关系链，适合于对组件化嵌入式系统进行安全性分析．
对ＳＥＦＴ顶层事件发生的概率特性进行定量分析是获得系统安全性参数的一种有效途径．但目前ＳＥＦＴ模型尚缺乏精确的语义描述，使得难以直接对其进行定量分析．由于ＳＥＦＴ既具有构件化特征又包含了系统的动
［５］
基金项目：江苏省研究生培养创新工程（Ｎｏ．ＣＸＺＺ１１－０２１８）；中央高校基本科研业务费专项资金（Ｎｏ．ＣＸＺＺ１１－０２１８，Ｎｏ．ＮＳ２０１２１２９）；国家自然科学基金（Ｎｏ．６１２７２０８３，Ｎｏ．６１１７００４３，Ｎｏ．６１１０００３４，Ｎｏ．６１２６２００２）；回国留学人员科研启动基金（２０１２）
态行为语义，也难以使用诸如二叉决策图（ＢｉｎａｒｙＤｅｃｉ－
［６］
ｓｉｏｎＤｉａｇｒａｍｓ，ＢＤＤ）等之类的方法对其精确描述和分析．已有分析方法采用ＰｅｔｒｉＮｅｔ对ＳＥＦＴ进行精确的语
［５］
义描述，但ＰｅｔｒｉＮｅｔ缺少精确描述ＳＥＦＴ构件之间消息交互的语义，使得在对ＳＥＦＴ中的模型元素进行语义描述之后仍需要专业人员手动修改才能够形成分析模型，难以快速有效地得到整个ＳＥＦＴ的形式语义模型．为此，本文工作提出了一种基于交互马尔可夫链（Ｉｎｔｅｒ－
［７］
ａｃｔｉｖｅＭａｒｋｏｖＣｈａｉｎ，ＩＭＣ）的ＳＥＦＴ分析方法，能够给出符合ＳＥＦＴ模型特征的形式语义模型并进行ＳＥＦＴ的自动定量分析．
２ 状态事件故障树
本节介绍状态事件故障树的基本建模元素，并给出一个状态事件故障树的应用实例．
状态事件故障树（ＳＥＦＴ）模型结合了基于状态的模型元素和故障树元素，在基于状态转换的基础上表达失效事件发生的因果链．其基本建模元素如图１所示，包括构件、状态、事件等，各
建模元素的具体含义见文献［５］．
利用ＳＥＦＴ可以对组件化嵌入式系统失效的因果关系链进行描述．图２给出飞机起落架收放系统中“起落架放不下来”这个失效结果的状态事件故障树．系统包含三个构件ｃｏｎｔｒｏｌ，分别是起落架操作手柄（Ｌａｎｄｉｎｇｇｅａｒ起落架信号灯ｈａｎｄｌｅ）、起落架控制器（Ｌａｎｄｉｎｇｇｅａｒｓｅｍａｐｈｏｒｅ（Ｌａｎｄｉｎｇ）ｇｅａｒ．起落架操作手ｃｏｎｔｒｏｌｌｅｒ）和柄由飞行员操作，用于控制发送起落架收起或者放下的信号；起落架控制器在接收到收起或者放下信号之后对起落架进行控制；起落架信号灯用于监控起落架控制器，在出现故障的时候发出预警．图２中ＳＥＦＴ顶层事件是“起落架放不下来”失效的发生，通过两个ＡＮＤ逻辑门连接三个构件自底向上描述了该失效发生的因果链．即飞机的起落架在收起的情况下，需要放下起落架，但起落架控制器出现故障并且信号灯没有正常预警从而导致起落架放不下来的失效发生．此外，各构件的内部行为通过有限状态机进行描述，该有限状态机
同时描述构件的动作与概率行为．
３ 接口交互马尔可夫链
本节中将ＩＭＣ的交互动作精化为输入、输出动作，
提出接口交互马尔可夫链模型，并定义其并行组合操作用于描述构件系统中的组合行为语义．
３畅１ Ｉｎｔｅｒｆａｃｅ－ＩＭＣ模型
接口交互马尔可夫链（Ｉｎｔｅｒｆａｃｅ－ＩＭＣ）对交互马尔可
夫链（ＩＭＣ）［７］
的交互动作语义进行了精化，将动作分为输入ａｂｌｅｄ、输出和内部动作且取消了输入使能（ｉｎｐｕｔ－ｅｎ是不可接受的）特性，明确地表示出在当前状态上哪些输入动作－．Ｉｎｔｅｒｆａｃｅ－ＩＭＣ形式定义如下：
定义１ 一个接口交互马尔可夫链Ｐ是一个五元
组（Ｓ，ｓ０，Ａ，→，→Ｍ），其中：（１）Ｓ是状态集合；（２）ｓ０
是
初始状态；（３）Ａ是动作集，其中Ａ＝（ＡＩ，Ａｏ，Ａｉｎｔ），ＡＩ
为
输入动作集，ＡＯ为输出动作集，Ａｉｎｔ
为内部动作集；（４）
Ｉｎｔｅｒｆａｃｅ→是交互转换集合Ｒ－ＩＭＣ为非输入使能．通常将（（ｎｏｎｉｎｐｕｔｓ，ａ，ｓ′）－ｅｎａｂｌｅｄ∈→记作ａ
）；（５）ｓ→Ｍ
ｓ′，
彻Ｓ×＞０×Ｓ是马尔可夫转换集合．通常将（ｓ，λ，ｓ′）∈→
Ｍ
记作ｓλ
Ｍ
ｓ′．
根据以上定义，图３（ａ）中Ｉｎｔｅｒｆａｃｅ－ＩＭＣＰ状态集为
Ｓ＝｛Ｓ１，Ｓ２，Ｓ３，Ｓ４｝；初始状态为Ｓ１；动作集Ａ中ＡＩ
＝｛ａ｝，ＡＯ
＝｛ｂ｝，Ａｉｎｔ
＝矱；交互转换集→＝｛（Ｓ２，ａ？，Ｓ３），（Ｍ
ＩｎｔｅｒｆａｃｅＳ３，ｂ！，－ＩＭＣＳ４）｝的直观语义描述为系统在初始状态；马尔可夫转换集→＝｛（Ｓ１，λ，Ｓ２）｝．该λ的指数分布的随机转换Ｓ１经过一个停留时间服从参数为后转换到Ｓ２状态，然后接收动作ａ转换到Ｓ３状态，最后通过输出动作３畅２ Ｉｎｔｅｒｆａｃｅ－ＩＭＣｂ转换到的并行组合
Ｓ４状态．
构件化系统往往由多个子构件组成，并行组合操作使得可以使用子构件的本地行为模型构建整个系统
的全局行为模型［８］
．下面给出Ｉｎｔｅｒｆａｃｅ－ＩＭＣ的并行组合
定义．
定义２ 可组合．当两个接口交互马尔可夫链Ｐ和
描述且同时描述功能和概率特性，使用Ｉｎｔｅｒｆａｃｅ－ＩＭＣ可对其进行精确语义描述．ＳＥＦＴ中含有两种转换边：一种是时序转换边；一种是因果转换边．对于时序转换边，其描述的是构件内部状态转换关系，可以使用Ｉｎｔｅｒｆａｃｅ－ＩＭＣ中的交互转换对其进行表示．对于概率延时的时序转换边，由于表达系统经过一个指数时间的概率延迟转换到下一状态，可使用Ｉｎｔｅｒｆａｃｅ－ＩＭＣ中的马尔可夫转换进行表示．对于表示构件之间事件触发关系的因果转换边，存在触发事件与被触发事件之间的关系．而在Ｉｎｔｅｒｆａｃｅ－ＩＭＣ中存在输入／输出动作的同步关系，所以能Ｑ满足ＡＯＰ∩ＡＯＱ＝ＡＩＰ∩ＡＩＱ＝ＡｉｎｔＰ∩ＡＱ＝ＡＰ∩Ａｉｎｔ
Ｑ＝矱时，则ｓｈａｒｅｄＰ（和ＰＱ，Ｑ可）＝组（Ａ合．同时记Ｐ和Ｑ的共享动作集
ＯＰ∩ＡＩＱ）∪（ＡＩＰ∩ＡＯ
Ｑ）．
Ｉｎｔｅｒｆａｃｅ 定义３ Ｉｎｔｅｒｆａｃｅ－ＩＭＣ的并行组合．Ｐ和Ｑ为两个Ｐ‖Ｑ为－ＩＭＣ（ＳＰ，×如Ｓ果ＱＰ０和Ｑ０可以组合，Ｉ则组合的Ｏ
结果
ｉｎｔ
，（ＳＰ，ＳＱ），（（Ｐ‖Ｑ），（Ｐ‖Ｑ），（Ｐ‖Ｑ）），→
Ｐ‖Ｑ
，→ＰＭ
‖Ｑ）其中：
瞯（Ｐ‖Ｑ）Ｉ＝（ＡＩ
Ｐ∪ＡＩ
Ｑ）＼（ＡＯ
Ｐ∪ＡＱＯ
）；瞯（Ｐ‖Ｑ）Ｏ
＝（ＡＯ
Ｐ∪ＡＯ
Ｑ）＼（ＡＩ
Ｐ∪ＡＱＩ
）瞯（Ｐ‖Ｑ）ｉｎｔ
＝Ａｉｎｔ
Ｐ∪Ａｉｎｔ
；
Ｑ∪（（ＡＩ
Ｐ∪ＡＩＱ）∩（ＡＰＯ∪ＡＱＯ
））；瞯→
Ｐ‖Ｑ
＝｛（ｓ，ｔａ
‖Ｑ
（ｓｓ
ａ
Ｐ
ｓＺａ∈ＡＰ＼ＡＱ｝
∪｛（ｓ，ｔａ
′，ｔ）｜Ｐ‖Ｑ
（ｓ，ｔｔａ∈ＡＱ＼ＡＰ｝∪｛（ｓ，ｔ）
ａ
′）｜ｔ
ａ
′∧Ｐ‖Ｑ
（ｓ′，ｔ′）｜ｓ
ａ
Ｐ
ｓ′∧ｔ
ａ
′∧ｔ′∧ａ∈ＡＱ∩ＡＰ｝；
瞯→Ｍｓ′，ｔ）｜ｓ
λ
Ｍ
Ｐ‖Ｑ＝｛（ｓ，
ｔλ
Ｍ
（Ｐｓ′｝∪｛（ｓ，
ｔλ
Ｍ
（ｓ，ｔ′）｜ｔλ
Ｍ
ｔ
′｝．根据以上并行组合规则，图３中的Ｐ和Ｑ并行组合结果为Ｐ‖Ｑ，如图３（ｃ）所示．
在Ｉｎｔｅｒｆａｃｅ－ＩＭＣ并行组合的过程中可能会出现这样一种情况：在某一个组合状态上的一个Ｉｎｔｅｒｆａｃｅ－ＩＭＣ相对于另一个Ｉｎｔｅｒｆａｃｅ－ＩＭＣ有输出动作时，后者并没有
相应的输入动作作为接收［８］
，这类组合状态称之为非法状态．在组合的过程中，需要去掉组合状态集中的非法状态．此外，在Ｉｎｔｅｒｆａｃｅ－ＩＭＣ并行组合的过程中可能会出现状态空间爆炸的情况．此时，可以采用状态约简技术化简所生成的状态空间．
４ 状态事件故障树（ＳＥＦＴ）的语义描述
对ＳＥＦＴ进行形式语义描述［９］
是对其进行分析的基础．本节使用上节中所建立的接口交互马尔可夫链（Ｉｎｔｅｒｆａｃｅ－ＩＭＣ）对ＳＥＦＴ的构件与逻辑门语义进行精确描述４畅１ ．
ＳＥＦＴ构件的语义
由于ＳＥＦＴ构件的内部行为使用有限状态机进行
够使用输入／输出动作的同步对因果转换边进行描述．
综上，采用Ｉｎｔｅｒｆａｃｅ－ＩＭＣ来描述ＳＥＦＴ构件语义的原则如下：
（１）使用Ｉｎｔｅｒｆａｃｅ－ＩＭＣ状态描述ＳＥＦＴ构件的状态．（２）使用Ｉｎｔｅｒｆａｃｅ－ＩＭＣ动作描述ＳＥＦＴ构件的事件．（３）使用Ｉｎｔｅｒｆａｃｅ－ＩＭＣ中的交互转换对ＳＥＦＴ构件内部时序边语义进行描述．
（４）使用Ｉｎｔｅｒｆａｃｅ－ＩＭＣ之间输出与输入动作发送与接收的同步对因果边语义进行描述．
４ＳＥＦＴ（畅２ 状态和事件端口的语义进行描述５）使用Ｉｎｔｅｒｆａｃｅ－ＩＭＣ中消息的输入输出类型对ＳＥＦＴ逻辑门的语义
．
下面使用Ｉｎｔｅｒｆａｃｅ－ＩＭＣ对ＳＥＦＴ逻辑门进行精确的语义描述．其中，每一种逻辑门的语义（记为［…］ＥＬＴ）是一个函数ｆａｃｅ－ＩＭＣ图４（模型，以若干动作作为输入，输出为相应的Ｉｎｔｅｒ－ａ）给出了两输入．
ＡＮＤ门（ＡＮＤ，２）的语义，即
函数［（ＡＮＤ，２）］ＥＬＴ：Ａ３
→Ｉｎｔｅｒｆａｃｅ－ＩＭＣ，以ＡＮＤ门的输出和两个输入信号作为参数．当ＡＮＤ门接收到两个输入信号时才会被触发．
图４（ｂ）给出了两输入ＯＲ门（ＯＲ，２）的语义，即函
第 ８ 期
３
徐丙凤：一种状态事件故障树的定量分析方法１４８３
数［（ＯＲ，２）］ＥＬＴ：Ａ→Ｉｎｔｅｒｆａｃｅ－ＩＭＣ，以ＯＲ门的输出和
两个输入信号为参数．当ＯＲ门接收到其中一个输入信号时ＯＲ门被触发．
图４（ｃ）中给出了两输入ＰＡＮＤ门（ＰＡＮＤ，２）的语
３
义，即函数［（ＰＡＮＤ，２）］ＥＬＴ：Ａ→Ｉｎｔｅｒｆａｃｅ－ＩＭＣ，以ＰＡＮＤ门的输出和两个输入作为参数．当ＰＡＮＤ门接收到以从左到右的顺序发生的两个输入信号时被触发．
图４（ｄ）给出了２／３ＶＯＴＩＮＧ门（ＶＯＴＩＮＧ，３，２）的语
４
义，即函数［（ＶＯＴＩＮＧ，３，２）］ＥＬＴ：Ａ→Ｉｎｔｅｒｆａｃｅ－ＩＭＣ，以ＶＯＴＩＮＧ门的输出和三个输入信号为参数．当ＶＯＴＩＮＧＯＯＩＩｉｎｔｉｎｔ
ＡＯＡｉｎｔＲ＝（ＡＰ∪ＡＱ）＼（ＡＰ∪ＡＱ）；Ｒ＝ＡＰ∪ＡＱ∪ｓｈａｒｅｄａｃｔｉｏｎ；
ｓ０Ｒ＝（ｓ０Ｐ，ｓ０Ｑ）；ＳＲ←ＳＲ∪Ｓ０Ｒ；
ｕｎｐｒｏｃｅｓｓｅｄ－ＳＲ←ＳＲ，ｓａｖｅｕｎｐｒｏｃｅｓｓｅｄｅｌｅｍｅｎｔｏｆＳＲ；
ｔｅｍｐ←ｓ０Ｒ，ｓａｖｅａｐａｉｒｏｆｅｌｅｍｅｎｔｓ，ｗｈｉｃｈｒｅｓｐｅｃｔｉｖｅｌｙｒｅｐｒｅｓｅｎｔｓｓｔａｔｅｏｆ ｒｅｐｅａｔ
Ｉｎｔｅｒｆａｃｅ－ＩＭＣＰａｎｄＱ；
ｐｉｃｋｏｎｅｕｎｐｒｏｃｅｓｓｅｄｅｌｅｍｅｎｔｔｅｍｐｆｒｏｍＳＲ；
ｓｒｅｐｒｅｓｅｎｔｓｔｈｅｆｉｒｓｔｅｌｅｍｅｎｔｏｆｔｅｍｐ，ｔｒｅｐｒｅｓｅｎｔｓｔｈｅｓｅｃｏｎｄｅｌｅｍｅｎｔｏｆｔｅｍｐ； ｉｆｓ
λ
ＭＰ
ｓ′ｔｈｅｎａｄｄ（ｓ′，ｔ）ｔｏＳＲａｎｄ（ｓ，ｔＲｉｆｔｈｅｙｄｏｎｏｔｅｘｉｓｔ
λ
λ
Ｍ
（ｓ′，ｔ）ｉｎ→
Ｍ
ｏｆ
λ
Ｍ
Ｍ
门接收到三个输入信号中的两个时ＶＯＴＩＮＧ门被触发．
５ ＳＥＦＴ的定量分析
本节介绍ＳＥＦＴ的定量分析方法．这里，ＳＥＦＴ模型
应为“合法模型”（判断ＳＥＦＴ是否合法的具体步骤见文献［５］）．对ＳＥＦＴ的逻辑门与构件都采用Ｉｎｔｅｒｆａｃｅ－ＩＭＣ进行了精确的语义描述之后ＳＥＦＴ，可通过并行组合得到到的模型进行定量分析的完整语义模型，再利用概率分析工具对最终得．以下对Ｉｎｔｅｒｆａｃｅ－ＩＭＣ并行组合以及５畅１ ＭＲＭＣＩｎｔｅｒｆａｃｅ定量计算进行详细介绍－ＩＭＣ并行组合
．
如前文所述，在进行Ｉｎｔｅｒｆａｃｅ－ＩＭＣ的并行组合过程中，可能存在两个构件接口之间交互不同步所形成的非法状态，在进行并行组合的过程中需要去掉这些非法状态ｆａｃｅ．本文并行组合算法思想为：状态－ＩＭＣ．然后根据定义的初始状态３，构造组合后首先组合两个Ｉｎｔｅｒ－的并行组合规则组合生成下一状Ｉｎｔｅｒｆａｃｅ－ＩＭＣ的初始态，在这里交替处理马尔可夫转换和动作转换，并在组合状态生成之后判断是否属于非法状态，若属于则去掉状态及相应转换ＩＭＣＲ．该算法的时间复杂度为Ｐ和Ｑ，通过并行组合得到，如算法１所示，给定两个Ｉｎｔｅｒｆａｃｅ－Ｏ（ｍＰ×和ｎ）Ｑ，其中的并行组合结果ｍ和ｎ分别是Ｐ和Ｑ的状态数．
在进行多个Ｉｎｔｅｒｆａｃｅ－ＩＭＣ的并行组合过程中，可能会出现状态空间爆炸的问题．为解决该问题，可进一步采用弱互模拟技术对组合结果Ｉｎｔｅｒｆａｃｅ－ＩＭＣ进行等价状态合并，得到一个与原Ｉｎｔｅｒｆａｃｅ－ＩＭＣ弱互摸拟的模型，然后再与其余的Ｉｎｔｅｒｆａｃｅ－ＩＭＣ进行并行组合．
算法１ ＣｏｍｐｕｔｉｎｇｐａｒａｌｌｅｌｃｏｍｐｏｓｉｔｉｏｎｏｆｔｗｏＩｎｔｅｒｆａｃｅ－ＩＭＣｓＩｎｐｕｔ：Ｐ＝（ＳＰ，ｓ０Ｐ，ＡＰ，→，→
Ｍ
）ａｎｄＱ＝（ＳＱ，ｓ０Ｑ，
ＡＱ，→，→Ｍ
）．
Ｏｕｔｐｕｔ：ＰａｒａｌｌｅｌｃｏｍｐｏｓｉｔｉｏｎｒｅｓｕｌｔＲ＝Ｐ‖Ｑ．Ｆｕｎｃｔｉｏｎ：ＰａｒａｌｌｅｌｃｏｍｐｏｓｉｎｇｔｗｏＩｎｔｅｒｆａｃｅ－ＩＭＣｓ
ｉｆＡＯＰ∩ＡＯＱ＝ＡｉｎｔＰ∩ＡＱ＝ＡＰ∩ＡｉｎｔＱ＝ＡＩＰ∩ＡＩＱ＝矱
ｔｈｅｎｂｅｇｉｎ
ｓｈａｒｅｄａｃｔｉｏｎ＝ＡＰ∩ＡＱ；ＡＩＲ＝（ＡＩＰ∪ＡＩＱ）＼（ＡＯＰ∪ＡＯＱ）；
ｉｆｔ
ｔ′ｔｈｅｎａｄｄ（ｓ，
ｔ′）ｔｏＳＲａｎｄ（ｓ，ｔ（ｓ，ｔ′）ｉｎ→
Ｍ
ｔｅｍｐｉｓｎｏｔｉｌｌｅｇａｌｉｆｔｈｅｙｓｔａｔｅｄｏｎｏｔｅｘｉｓｔ
ｏｆＲ
ｉｆ ｔｈｅｎｂｅｇｉｎ ｉｆｓ
ａ
Ｐ
ｓ′∧ａ∈ＡＰ＼ＡＱｔｈｅｎａｄｄ（ｓ′，ｔ）ｔｏＳＲａ
ａｎｄ（ｓ，ｔ）
Ｐ‖Ｑ（ｓ′
，ｔ）ｔｏ→ｏｆＲ
ｉｆｔ
ａ
ｔ′∧ａ∈ＡＱ＼ＡＰｔｈｅｎａｄｄ（ｓ，ｔ′）ｔｏＳＲａ
ａｎｄ（ｓ，ｔ）
‖Ｑ（ｓ
，ｔ′）ｔｏ→ｏｆＲ
ｉｆｓ
ａ
Ｐ
ｓ′∧ｔ
ａ
ｔ′∧ａ∈ＡＱ∩ＡＰｔｈｅｎａｄｄ（ｓ′，ｔ′）ｔｏＳＲ
ａ
Ｐ‖Ｑ（ｓ′
→ｏｆＲ
ｅｎｄａｎｄ（ｓ，ｔ，ｔ′）ｔｏ ｅｌｓｅｂｅｇｉｎ
ｒｅｍｏｖｅｔｒａｎｓｉｔｉｏｎｔｏｔｅｍｐｆｒｏｍ→ｏｆＲ； ｉｆｔｅｍｐｄｏｅｓｎｏｔａｐｐｅａｒｉｎ→Ｍ
ｅｎｄ
ｏｆＲｔｈｅｎｒｅｍｏｖｅｔｅｍｐｆｒｏｍＳＲ
ｕｐｄａｔｅｕｎｐｒｏｃｅｓｓｅｄ－ＳＲ； ｕｎｔｉｌｕｎｐｒｏｃｅｓｓｅｄ－ＳＲ＝矱 ｅｎｄｒｅｔｕｒｎＲｅｌｓｅｒｅｔｕｒｎｆａｌｓｅ
５畅２ ＳＥＦＴ的概率特性计算
对ＳＥＦＴ的定量分析即计算顶层事件发生的概率特性ＳＥＦＴ．在采用Ｉｎｔｅｒｆａｃｅ－ＩＭＣ描述ＳＥＦＴ的语义模型之后，作，而的顶层事件在构件中输出动作的发生通常认为没有时间延迟Ｉｎｔｅｒｆａｃｅ－ＩＭＣ中表示为一个输出动．因此，计算ＳＥＦＴ顶层事件发生的概率就等同于计算在给定时间区间内，从ＳＥＦＴ的形式语义模型的初始状态到达该输出动作的出发状态的概率是否在可接受的范围内．
从ＳＥＦＴ构件和逻辑门的形式语义模型的并行组合过程中可以看出，除了描述ＳＥＦＴ顶层事件的输出动作未形成内部动作，其他所有的输入输出动作都经过同步成为内部动作．因此在最终用于定量计算的ＳＥＦＴ语义模型中，只有表示顶层事件语义的一个输出动作．注意到该输出动作的出发状态即为分析的目标状态，
１４８４ 电 子 学 报２０１３年
因而在分析模型中并不需要包含表示顶层事件语义的输出动作．此时从初始状态到目标状态之间所有的转换都为马尔可夫转换．因此，最后分析的模型实际上是一个不包含交互动作的连续时间马尔可夫链（Ｃｏｎｔｉｎｕ－
［１０］
ｏｕｓＴｉｍｅＭａｒｋｏｖＣｈａｉｎ，ＣＴＭＣ）模型．
［１１］
本文利用ＭＲＭＣ对所得到的ＣＴＭＣ模型进行特定时间区间内从初始状态到目标状态的概率计算．具体包括：采用组合结果的初始状态作为进行分析的初始状态；根据ＳＥＦＴ中顶层事件所对应的输出动作确定在ＳＥＦＴ的语义模型中该输出动作的出发状态，作为目执行，无需人工参与手动修改．
６ 实例研究
本节针对图２中给出的飞机起落架收放系统的
ＳＥＦＴ，利用文章所提出的方法对其进行定量分析．为表述清晰，根据本文方法的处理流程给出完整的执行过程描述．
首先对于图２中的ＳＥＦＴ采用Ｉｎｔｅｒｆａｃｅ－ＩＭＣ给出其精确语义．该ＳＥＦＴ中一共包含３个构件与２个逻辑门，利用Ｉｎｔｅｒｆａｃｅ－ＩＭＣ精确描述３个构件与２个逻辑门的语标状态；给定需要分析的时间区间以及概率范围；编写符合ＭＲＭＣＭＲＭＣ示在给定的时间内得到概率计算的结果输入文件规范的，顶层事件发生的概率是否在可接．在ＣＴＭＣＳＥＦＴ模中该概率特性表型文件，使用受的范围内．该定量计算结果可以为评估系统安全性提供参考．
综上所述，图５中给出了本文所提出的ＳＥＦＴ定量分析方法的具体处理流程．首先得到状态事件故障树的ＸＭＬ形式的模型文件，通过解析模型文件，提取建立各构件和逻辑门的Ｉｎｔｅｒｆａｃｅ－ＩＭＣ模型所需要的信息．然后，对各构件的Ｉｎｔｅｒｆａｃｅ－ＩＭＣ模型进行并行组合以及状态约简ｔｅｒｆａｃｅ，得到最终的ＳＥＦＴ语义模型．在得到ＳＥＦＴ的Ｉｎ－具对其进行计算－ＩＭＣ语义模型之后，得到计算结果，调用已有的概率模型分析工，即ＳＥＦＴ中顶层事件的概率特性．可以看出，在该处理流程中，得到ＳＥＦＴ模型的ＸＭＬ文件之后，整个过程可以完全通过程序自动
义如图６所示．论文根据ＳＥＦＴ中的构件与逻辑门的层次从下到上对得到的Ｉｎｔｅｒｆａｃｅ－ＩＭＣ进行编号．可以看出，对该ＳＥＦＴ的顶层事件发生概率的计算对应到其形式语义模型中即计算Ｃ５中Ｓ３状态的概率特性．在得到ＳＥＦＴ中各个元素的Ｉｎｔｅｒｆａｃｅ－ＩＭＣ形式语义模型之后ＳＥＦＴ，通（（（Ｃ的完过对这些整语义Ｉｎｔｅｒｆａｃｅ‖Ｃ模型－．ＩＭＣｓ本实进行并行组合操作得到例设定的组合顺序为：２‖Ｃ１）４）‖Ｃ５）‖Ｃ３，每进行一步组合利用弱互模拟操作对组合之后的Ｉｎｔｅｒｆａｃｅ－ＩＭＣ进行约简，将约简的结果再进行下一次组合，以此类推，形成最终组合结果．整个并行组合以及约简过程如图７所示．由于在该实例中，ｆ５！是顶层逻辑门的输出，计算ＳＥＦＴ的顶层事件概率即计算图７（８）中Ｓ３状态的概率特性．下面采用ＭＲＭＣ对图７（８）
进行定量计算．
ＩＭＣ参数是在给定的时间区间内目标状态发生的概率是否语义模型中目标状态发生的概率ＳＥＦＴ中顶层事件发生的概率即ＳＥＦＴ，可以得到的概率的Ｉｎｔｅｒｆａｃｅ－在预期的范围内．例如：图７（８）中λ和μ的取值分别为０畅０２和０畅０１．分析在［０，１００００］时间区间内，从初始状态到达目标状态的概率是否小于０畅０００１．利用ＭＲＭＣ分析的结果如图ｔｒａ单位内中的１，从初始状态状态为符合要求的状态８所示．由图８中的结果可以看出１到达目标状态．即在［０４的概率小于，１００００］，时间ａｌｇｓ．０畅０００１．因此，对应到ＳＥＦＴ中，即在［０，１００００］时间区间内，顶层事件发生的概率小于０畅０００１．其物理含义为起
因而在分析模型中并不需要包含表示顶层事件语义的输出动作．此时从初始状态到目标状态之间所有的转换都为马尔可夫转换．因此，最后分析的模型实际上是一个不包含交互动作的连续时间马尔可夫链（Ｃｏｎｔｉｎｕ－
［１０］
ｏｕｓＴｉｍｅＭａｒｋｏｖＣｈａｉｎ，ＣＴＭＣ）模型．
［１１］
本文利用ＭＲＭＣ对所得到的ＣＴＭＣ模型进行特定时间区间内从初始状态到目标状态的概率计算．具体包括：采用组合结果的初始状态作为进行分析的初始状态；根据ＳＥＦＴ中顶层事件所对应的输出动作确定在ＳＥＦＴ的语义模型中该输出动作的出发状态，作为目执行，无需人工参与手动修改．
６ 实例研究
本节针对图２中给出的飞机起落架收放系统的
ＳＥＦＴ，利用文章所提出的方法对其进行定量分析．为表述清晰，根据本文方法的处理流程给出完整的执行过程描述．
首先对于图２中的ＳＥＦＴ采用Ｉｎｔｅｒｆａｃｅ－ＩＭＣ给出其精确语义．该ＳＥＦＴ中一共包含３个构件与２个逻辑门，利用Ｉｎｔｅｒｆａｃｅ－ＩＭＣ精确描述３个构件与２个逻辑门的语标状态；给定需要分析的时间区间以及概率范围；编写符合ＭＲＭＣＭＲＭＣ示在给定的时间内得到概率计算的结果输入文件规范的，顶层事件发生的概率是否在可接．在ＣＴＭＣＳＥＦＴ模中该概率特性表型文件，使用受的范围内．该定量计算结果可以为评估系统安全性提供参考．
综上所述，图５中给出了本文所提出的ＳＥＦＴ定量分析方法的具体处理流程．首先得到状态事件故障树的ＸＭＬ形式的模型文件，通过解析模型文件，提取建立各构件和逻辑门的Ｉｎｔｅｒｆａｃｅ－ＩＭＣ模型所需要的信息．然后，对各构件的Ｉｎｔｅｒｆａｃｅ－ＩＭＣ模型进行并行组合以及状态约简ｔｅｒｆａｃｅ，得到最终的ＳＥＦＴ语义模型．在得到ＳＥＦＴ的Ｉｎ－具对其进行计算－ＩＭＣ语义模型之后，得到计算结果，调用已有的概率模型分析工，即ＳＥＦＴ中顶层事件的概率特性．可以看出，在该处理流程中，得到ＳＥＦＴ模型的ＸＭＬ文件之后，整个过程可以完全通过程序自动
义如图６所示．论文根据ＳＥＦＴ中的构件与逻辑门的层次从下到上对得到的Ｉｎｔｅｒｆａｃｅ－ＩＭＣ进行编号．可以看出，对该ＳＥＦＴ的顶层事件发生概率的计算对应到其形式语义模型中即计算Ｃ５中Ｓ３状态的概率特性．在得到ＳＥＦＴ中各个元素的Ｉｎｔｅｒｆａｃｅ－ＩＭＣ形式语义模型之后ＳＥＦＴ，通（（（Ｃ的完过对这些整语义Ｉｎｔｅｒｆａｃｅ‖Ｃ模型－．ＩＭＣｓ本实进行并行组合操作得到例设定的组合顺序为：２‖Ｃ１）４）‖Ｃ５）‖Ｃ３，每进行一步组合利用弱互模拟操作对组合之后的Ｉｎｔｅｒｆａｃｅ－ＩＭＣ进行约简，将约简的结果再进行下一次组合，以此类推，形成最终组合结果．整个并行组合以及约简过程如图７所示．由于在该实例中，ｆ５！是顶层逻辑门的输出，计算ＳＥＦＴ的顶层事件概率即计算图７（８）中Ｓ３状态的概率特性．下面采用ＭＲＭＣ对图７（８）
进行定量计算．
ＩＭＣ参数是在给定的时间区间内目标状态发生的概率是否语义模型中目标状态发生的概率ＳＥＦＴ中顶层事件发生的概率即ＳＥＦＴ，可以得到的概率的Ｉｎｔｅｒｆａｃｅ－在预期的范围内．例如：图７（８）中λ和μ的取值分别为０畅０２和０畅０１．分析在［０，１００００］时间区间内，从初始状态到达目标状态的概率是否小于０畅０００１．利用ＭＲＭＣ分析的结果如图ｔｒａ单位内中的１，从初始状态状态为符合要求的状态８所示．由图８中的结果可以看出１到达目标状态．即在［０４的概率小于，１００００］，时间ａｌｇｓ．０畅０００１．因此，对应到ＳＥＦＴ中，即在［０，１００００］时间区间内，顶层事件发生的概率小于０畅０００１．其物理含义为起
状态事件故障树（Ｓｔａｔｅ／ＥｖｅｎｔＦａｕｌｔＴｒｅｅ，ＳＥＦＴ）将传统故
障树中的元素与基于状态的模型元素结合起来，同时描述构件化系统的行为模型和失效因果链．
在定量分析方面，由于ＦＴ、ＤＦＴ以及ＳＥＦＴ都缺乏形式语义，难以直接对它们进行定量分析，通常采用具
［１２，１３］
精确描述其语义再进行有精确语义的形式化模型
分析．如：文献［３］基于ＢＤＤ分析ＦＴ的概率特征；文献［１４］基于马尔可夫链分析ＤＦＴ的概率特征．而对于ＳＥＦＴ的定量分析文献［５］采用ＰｅｔｒｉＮｅｔ对其进行定量分析，在对ＳＥＦＴ中的构件和逻辑门进行语义描述之落架收放系统不发生“起落架放不下来”失效的概率高于９９畅９９％，该参数可以为评估该系统的安全性提供参
考．
７ 相关工作
对嵌入式软件进行安全性分析是软件开发过程中
的重要步骤．故障树（ＦａｕｌｔＴｒｅｅ，ＦＴ）［３］
是当前工业界安全性分析过程中应用最广泛的技术，但由于故障树在动态系统以及构件化系统方面的表达能力不足，已存在一系列基于故障树的安全性建模分析技术，包括：动态故障树（ＤｙｎａｍｉｃＦａｕｌｔＴｒｅｅ，ＤＦＴ）［４］、构件故障树
（ＣｏｍｐｏｎｅｎｔＦａｕｌｔＴｒｅｅ，ＣＦＴ）［５］
等．但以上方法仍缺乏描述构件化系统中建模事件顺序以及状态依赖的能力．
后，仍需对所得到的ＰｅｔｒｉＮｅｔ构件进行手动修改并且手动合并生成完整ＳＥＦＴ语义模型，整个过程难以自动有效地进行．与已有的工作相比，本文根据ＳＥＦＴ的特点设计接口交互马尔可夫链对其语义进行描述并设计相应的定量分析方法对其进行定量分析，且整个过程可由程序自动完成，无需人工参与手动修改与合并．
８ 总结
本文针对状态事件故障树的定量分析提出了一种新的解决方法．首先通过对交互马尔可夫链的交互动作进行精化，提出了接口交互马尔可夫链模型；其次采用接口交互马尔可夫链对ＳＥＦＴ构件与逻辑门的语义进行精确描述，并通过并行组合得到整个ＳＥＦＴ的语义模型；再利用概率模型分析工具ＭＲＭＣ对ＳＥＦＴ的语义模型进行定量分析，完成对ＳＥＦＴ顶层事件在给定时间内发生的概率进行分析；最终以一个系统实例讨论该方法的可行性．
参考文献
［１］陈火旺，王戟，董威．高可信软件工程技术［Ｊ］．电子学报，
２００３，３１（１２Ａ）：１９３３－１９３８．ＣｈｅｎＨｕｏ－ｗａｎｇ，ＷａｎｇＪｉ，ＤｏｎｇＷｅｉ．Ｈｉｇｈｃｏｎｆｉｄｅｎｃｅｓｏｆｔｗａｒｅｅｎｇｉｎｅｅｒｉｎｇｔｅｃｈｎｏｌｏｇｉｅｓ［Ｊ］．ＡｃｔａＥｌｅｃｔｒｏｎｉｃａＳｉｎｉｃａ，２００３，３１（１２Ａ）：１９３３－１９３８．（ｉｎＣｈｉｎｅｓｅ）［２］ＭａｈｍｏｏｄＳ，ＬａｉＲ，ＳｏｏＫｉｍＹ，ｅｔａｌ．Ａｓｕｒｖｅｙｏｆｃｏｍｐｏｎｅｎｔ
ｂａｓｅｄｓｙｓｔｅｍｑｕａｌｉｔｙａｓｓｕｒａｎｃｅａｎｄａｓｓｅｓｓｍｅｎｔ［Ｊ］．ＩｎｆｏｒｍａｔｉｏｎａｎｄＳｏｆｔｗａｒｅＴｅｃｈｎｏｌｏｇｙ，２００５，４７（１０）：６９３－７０７．［３］ＲｅａｙＫＡ，ＡｎｄｒｅｗｓＪＤ．Ａｆａｕｌｔｔｒｅｅａｎａｌｙｓｉｓｓｔｒａｔｅｇｙｕｓｉｎｇｂｉ－
ｎａｒｙｄｅｃｉｓｉｏｎｄｉａｇｒａｍｓ［Ｊ］．ＲｅｌｉａｂｉｌｉｔｙＥｎｇｉｎｅｅｒｉｎｇ＆ＳｙｓｔｅｍＳａｆｅｔｙ，２００２，７８（１）：４５－５６．［４］ˇＣｅｐｉｎＭ，ＭａｖｋｏＢ．Ａｄｙｎａｍｉｃｆａｕｌｔｔｒｅｅ［Ｊ］．ＲｅｌｉａｂｉｌｉｔｙＥｎｇｉ－ｎｅｅｒｉｎｇ＆ＳｙｓｔｅｍＳａｆｅｔｙ，２００２，７５（１）：８３－９１．［５］ＫａｉｓｅｒＢ．ＳｔａｔｅＥｖｅｎｔｔｒｅｅｓ：Ａｓａｆｅｔｙａｎｄｒｅｌｉａｂｉｉｔｙａｎａｌｙｓｉｓ
ｔｅｃｈｎｉｑｕｒｅｆｏｒｓｏｆｔｗａｒｅｃｏｎｔｒｏｌｌｅｄｓｙｓｔｅｍｓ［Ｄ］．Ｋａｉｓｅｒ－ｓｌａｕｔｅｒｎ：Ｕｎｉｖｅｒｓｉｔ惫ｔＫａｉｓｅｒｓｌａｕｔｅｒｎ，２００７．［６］ＢｒｙａｎｔＲＥ．Ｇｒａｐｈ－ｂａｓｅｄａｌｇｏｒｉｔｈｍｓｆｏｒＢｏｏｌｅａｎｆｕｎｃｔｉｏｎｍａ－
ｎｉｐｕｌａｔｉｏｎ［Ｊ］．ＩＥＥＥＴｒａｎｓａｃｔｉｏｎｓｏｎＣｏｍｐｕｔｅｒｓ，１９８６，１００
（８）：６７７－６９１．［７］ＨｅｒｓｍａｎｓＨ．ＩｎｔｅｒａｃｔｉｖｅＭａｒｋｏｖＣｈａｉｎｓ［Ｍ］．Ｂｅｒｌｉｎ：Ｓｐｒｉｎｇｅｒ－
Ｖｅｒｌａｇ，２００２．５７－８８．［８］ＤｅＡｌｆａｒｏＬ，ＨｅｎｚｉｎｇｅｒＴＡ．Ｉｎｔｅｒｆａｃｅａｕｔｏｍａｔａ［Ａ］．Ｐｒｏｃｅｅｄ－
ｉｎｇｓｏｆｔｈｅＪｏｉｎｔ８ｔｈＥｕｒｏｐｅａｎＳｏｆｔｗａｒｅＥｎｇｉｎｅｅｒｉｎｇＣｏｎｆｅｒｅｎｃｅａｎｄ９ｔｈＡＣＭＳＩＧＳＯＦＴＩｎｔｅｒｎａｔｉｏｎａｌＳｙｍｐｏｓｉｕｍｏｎｔｈｅＦｏｕｎ－ｄａｔｉｏｎｓｏｆＳｏｆｔｗａｒｅＥｎｇｉｎｅｅｒｉｎｇ（ＥＳＥＣ／ＦＳＥ０１）［Ｃ］．ＮｅｗＹｏｒｋ：ＡＣＭＰｒｅｓｓ，２００１，１０９－１２０．［９］周颖，郑国梁，李宣东．面向模型检验的ＵＭＬ状态机语义
［Ｊ］．ＪｏｕｒｎａｌｏｆＣｏｍｐｕｔｅｒＲｅｓｅａｒｃｈａｎｄＤｅｖｅｌｏｐｍｅｎｔ，２００８，４５（１０）：１６３８－１６４５．（ｉｎＣｈｉｎｅｓｅ）［１４］ＢｏｕｄａｌｉＨ，ＣｒｏｕｚｅｎＰ，ＳｔｏｅｌｉｎｇａＭ．Ａｒｉｇｏｒｏｕｓ，ｃｏｍｐｏｓｉｔｉｏｎ－
ａｌ，ａｎｄｅｘｔｅｎｓｉｂｌｅｆｒａｍｅｗｏｒｋｆｏｒｄｙｎａｍｉｃｆａｕｌｔｔｒｅｅａｎａｌｙｓｉｓ［Ｊ］．ＩＥＥＥＴｒａｎｓａｃｔｉｏｎｓｏｎＤｅｐｅｎｄａｂｌｅａｎｄＳｅｃｕｒｅＣｏｍｐｕｔ－ｉｎｇ，２０１０，７（２）：１２８－１４３
．作者简介
徐丙凤 女，１９８６年生于安徽安庆市．现为［Ｊ］．电子学报，２００３，３１（１２Ａ）：２０９１－２０９５．ＺｈｏｕＹｉｎｇ，ＺｈｅｎｇＧｕｏ－ｌｉａｎｇ，ＬｉＸｕａｎ－ｄｏｎｇ．Ａｎｏｐｅｒａｔｉｏｎａｌｓｅ－ｍａｎｔｉｃｓｆｏｒＵＭＬｓｔａｔｅｍａｃｈｉｎｅｓｉｎｍｏｄｅｌｃｈｅｃｋｉｎｇｃｏｎｔｅｘｔ［Ｊ］．ＡｃｔａＥｌｅｃｔｒｏｎｉｃａＳｉｎｉｃａ，２００３，３１（１２Ａ）：２０９１－２０９５．（ｉｎＣｈｉｎｅｓｅ）［１０］ＢａｉｅｒＣ，ＨａｖｅｒｋｏｒｔＢ，ＨｅｒｍａｎｎｓＨ，ｅｔａｌ．Ｍｏｄｅｌ－ｃｈｅｃｋｉｎｇａｌ－
ｇｏｒｉｔｈｍｓｆｏｒｃｏｎｔｉｎｕｏｕｓ－ｔｉｍｅＭａｒｋｏｖｃｈａｉｎｓ［Ｊ］．ＩＥＥＥＴｒａｎｓ－ａｃｔｉｏｎｓｏｎＳｏｆｔｗａｒｅＥｎｇｉｎｅｅｒｉｎｇ，２００３，２９（６）：５２４－５４１．［１１］ＫａｔｏｅｎＪＰ，ＫｈａｔｔｒｉＭ，ＺａｐｒｅｅｖｔＩ．ＡＭａｒｋｏｖｒｅｗａｒｄｍｏｄｅｌ
ｃｈｅｃｋｅｒ［Ａ］．ＰｒｏｃｅｅｄｉｎｇｓｏｆｔｈｅＳｅｃｏｎｄＩｎｔｅｒｎａｔｉｏｎａｌＣｏｎｆｅｒ－ｅｎｃｅｏｎｔｈｅＱｕａｎｔｉｔａｔｉｖｅＥｖａｌｕａｔｉｏｎｏｆＳｙｓｔｅｍｓ（ＱＥＳＴ’０５）［Ｃ］．Ｔｏｒｉｎｏ：ＩＥＥＥＣｏｍｐｕｔｅｒＳｏｃｉｅｔｙ，２００５．２４３－２４４．［１２］张广泉，戎玫，朱雪阳，何亚丽，石慧娟．基于ＸＹＺ／ＡＤＬ
的Ｗｅｂ服务组合描述与验证［Ｊ］．电子学报，２０１１，３９（３Ａ）：８６－９３．
ＺｈａｎｇＧｕａｎｇ－ｑｕａｎ，ＲｏｎｇＭｅｉ，ＺｈｕＸｕｅ－ｙａ，ＨｅＹａ－ｌｉ，ＳｈｉＨｕｉ－ｊｕａｎ．Ｓｐｅｃｉｆｉｃａｔｉｏｎａｎｄｖｅｒｉｆｉｃａｔｉｏｎｏｆｗｅｂｓｅｒｖｉｃｅｃｏｍｐｏ－ｓｉｔｉｏｎｂａｓｅｄｏｎＸＹＺ／ＡＤＬ［Ｊ］．ＡｃｔａＥｌｅｃｔｒｏｎｉｃａＳｉｎｉｃａ，２０１１，３９（３Ａ）：８６－９３．（ｉｎＣｈｉｎｅｓｅ）［１３］张君华，黄志球，曹子宁．模型检测基于概率时间自动机
的反例产生研究［Ｊ］．计算机研究与发展，２００８，４５（１０）：１６３８－１６４５．ＺｈａｎｇＪｕｎ－ｈｕａ，ＨｕａｎｇＺｈｉ－ｑｉｕ，ＣａｏＺｉ－ｎｉｎｇ．Ｃｏｕｎｔｅｒｅｘａｍｐｌｅｇｅｎｅｒａｔｉｏｎｆｏｒｐｒｏｂａｂｉｌｉｓｔｉｃｔｉｍｅｄａｕｔｏｍａｔａｍｏｄｅｌｃｈｅｃｋｉｎｇ
南京航空航天大学计算机科学与技术学院在读博士生．研究方向为软件工程，软件安全性分析与验证．
Ｅ－ｍａｉｌ：ｘｕｂｉｎｇｆｅｎｇ＠ｎｕａａ．ｅｄｕ
．
ｃｎ黄志球 男，１９６５年生于江苏南京人．在国防科学技术大学获工学学士和工学硕士学位，现为南京航空航天大学教授，博士生导师．主要研究方向为软件工程，服务计算，形式化方法，嵌入
式软件分析与验证．
胡 军（通信作者） 男，１９７３年生于湖北黄冈．南京大学计算机科学与技术系获计算机软件与理论博士学位，现为南京航空航天大学副教授，硕士生导师．主要研究方向为软件工程．软件分析与验证和嵌入式系统设计与分析．Ｅ－ｍａｉｌ：ｈｕｊｕｎ＠ｎｕａａ．ｅｄｕ．ｃｎ
一种状态事件故障树的定量分析方法
作者：作者单位：
徐丙凤， 黄志球， 胡军， 魏欧， 肖芳雄， XU Bing-feng， HUANG Zhi-qiu， HU Jun，WEI Ou， XIAO Fang-xiong
徐丙凤,黄志球,魏欧,XU Bing-feng,HUANG Zhi-qiu,WEI Ou(南京航空航天大学计算机科学与技术学院,江苏南京,210016)， 胡军,HU Jun(南京航空航天大学计算机科学与技术学院，江苏南京210016; 南京大学计算机软件新技术国家重点实验室，江苏南京 210093)， 肖芳雄,XIAO Fang-xiong(南京航空航天大学计算机科学与技术学院，江苏南京210016; 广西财经学院信息与统计学院，广西南宁530003)电子学报
Acta Electronica Sinica2013(8)
刊名：英文刊名：年，卷(期)：
参考文献(14条)
1.陈火旺,王戟,董威 高可信软件工程技术[期刊论文]-电子学报 2003(z1)
2.Sajjad Mahmood;Richard Lai;Yong Soo Kim;Ji Hong Kim;Seok Cheon Park;Hae Suk Oh A survey ofcomponent based system quality assurance and assessment[外文期刊] 2005(10)
3.Reay KA;Andrews JD A fault tree analysis strategy using bi-nary decision diagrams 2002(01)4.Marko Cepin;Borut Mavko A dynamic fault tree[外文期刊] 2002(1)
5.Kaiser B State Event trees:A safety and reliabiity analysis techniqure for software controlledsystems 2007
6.Bryant R E Graph-based algorithms for Boolean function ma-nipulation 1986(08)7.Hersmans H Interactive Markov Chains 20028.De Alfaro L;Henzinger T A Interface automata 2001
9.周颖,郑国梁,李宣东 面向模型检验的UML状态机语义[期刊论文]-电子学报 2003(z1)
10.Baier C;Haverkort B;Hermanns H Model-checking al-gorithms for continuous-time Markov chains2003(06)
11.Katoen JP;Khattri M;Zapreevt I A Markov reward model checker 2005
12.张广泉,戎玫,朱雪阳,何亚丽,石慧娟 基于XYZ/ADL的Web服务组合描述与验证[期刊论文]-电子学报 2011(z1)13.张君华,黄志球,曹子宁 模型检测基于概率时间自动机的反例产生研究[期刊论文]-计算机研究与发展 2008(10)14.Boudali H;Crouzen P;Stoelinga M A rigorous,composition-al,and extensible framework for dynamicfault tree analysis 2010(02)
引证文献(2条)
1.罗燕,刘庆华,谢跃雷 故障树分析法在列车数据展示中心的应用[期刊论文]-桂林电子科技大学学报 2014(02)2.崔铁军,马云东 空间故障树的径集域与割集域的定义与认识[期刊论文]-中国安全科学学报 2014(04)
引用本文格式：徐丙凤.黄志球.胡军.魏欧.肖芳雄.XU Bing-feng.HUANG Zhi-qiu.HU Jun.WEI Ou.XIAO Fang-xiong
一种状态事件故障树的定量分析方法[期刊论文]-电子学报 2013(8)