基于顺序逻辑的状态事件故障树定性分析模型

范亚琼，陈海燕

(南京航空航天大学 计算机科学与技术学院,江苏 南京 210016)

基于顺序逻辑的状态事件故障树定性分析模型

范亚琼，陈海燕

(南京航空航天大学 计算机科学与技术学院,江苏 南京 210016)

针对现有的状态事件故障树(SEFT)定性分析方法在反映失效系统中构件状态与事件逻辑顺序关系方面的不足，提出了基于顺序逻辑的状态事件故障树定性分析模型。该模型通过建立构件与逻辑门的端口映射表，定义逻辑门到布尔逻辑的转换规则限定状态和事件的次序关系，根据顺序逻辑转换规则获得导致系统失效的状态事件序列(最小割序集)，以解决系统失效应满足的状态与事件的逻辑顺序关系问题。为验证所提出模型的有效性和可行性，以火灾防护系统为研究对象进行了实例验证实验。实验结果表明，所提出的模型有效可行，所获得的最小割序集能够反映各失效事件和状态间的顺序逻辑关系，分析结果符合客观实际，为SEFT的定性分析提供了一种新的技术途径和方法借鉴。

顺序逻辑；端口映射表；最小割序集；转换规则；定性分析

0 引 言

状态事件故障树[1](State/Event Fault Tree，SEFT)是基于软件的构件设计模型建立的一种表达系统失效行为的安全性分析模型。与传统的故障树[2-4]不同的是，状态事件故障树具有构件化和基于状态的特性，且严格区分了状态、事件语义，增加了状态依赖的表达。因此，对状态事件故障树进行最小割序集分析不仅要关注构件失效的集合，也要关注构件失效事件和状态间的顺序关系，即分析出最小割序集。目前国内外安全分析领域的研究人员对SEFT的定性分析进行了相关研究。Michael Roth[5-6]提出将SEFT转换到确定随机Petri网(Deterministic and Stochastic Petri Nets，DSPN)，在DSPN的基础上计算其顺序逻辑并分析导致系统失效的最小割序集，但是该最小割序集只关注失效事件，未涉及失效事件发生时相关构件应满足的状态；徐博士[7]提出基于接口自动机的软件失效行为安全性分析模型。该模型考虑构件状态作为卫式条件对逻辑门输出产生的影响，计算过程繁琐，且最小割序集中未能反映状态和事件间的次序关系。

为此，提出了基于顺序逻辑的状态事件故障树定性分析模型。该模型通过分析构件与外界环境交互的状态或事件，建立逻辑门与构件端口相关联的端口映射表，定义逻辑门的转换规则，通过扩展布尔逻辑提出顺序逻辑转换规则，自顶向下计算分析整体系统的失效序列，通过化简操作获得系统的最小割序集。

1 问题描述

对软件失效行为进行安全性分析的目的是寻找导致软件系统失效的关键事件集合，即最小割序集[7]。作为反映构件失效逻辑层次关系的逻辑门，是定性分析的关键所在。

在SEFT中，构件的状态虽不能和事件一样触发逻辑门输出的发生，但是它可以允许或禁止逻辑门输出的发生。在进行SEFT定性分析的过程中，需要同时考虑构件的基本事件以及部分可作为卫式的构件状态。

对于状态事件混合逻辑门，其状态与事件存在顺序关系，当卫式条件成立时，失效事件的发生导致逻辑门产生输出，当卫士条件不成立时，失效事件的发生不会导致逻辑门产生输出。

2 基于顺序逻辑的SEFT定性分析模型

在状态事件故障树中，顶层事件的发生依赖于基本事件的发生顺序，而逻辑门中的卫式条件决定了发生的基本事件是否能对全局系统失效产生影响。提出了基于顺序逻辑[8]的SEFT定性分析模型，通过记录构件与逻辑门的交互端口，将逻辑门转换成布尔逻辑表达式，根据顺序逻辑转换规则，分析引起系统失效的最小关键状态事件序列。

2.1 端口映射表

构件与外界环境的交互分为三种：构件与构件之间的触发交互、构件与逻辑门的交互、逻辑门与逻辑门的交互。对SEFT进行定性分析，只需关注引起系统失效的关键事件或状态，对于构件内部的行为活动，若不产生外部输出，则不影响定性分析的结果。构件与外界环境的交互通过输入输出端口实现，因此，通过端口映射表建立构件和逻辑门与外界交互的关系。端口映射表的建立分三步完成：

(1)当系统规模较大时，为了方便引用，对构件和逻辑门进行编号。

(2)对于每个构件，记录与外界环境交互的关键事件或状态，若每个构件的交互端口较少，只需建立一个表存放所有的构件交互行为，若构件的交互端口较多，可为每一个构件建立一个组件端口映射表，表中说明构件编号、源端口、目的端口、状态事件类型、输入输出方向、具体行为。

(3)对每个逻辑门，记录与外界交互的端口，若每个逻辑门的交互端口较少，只需建立一张表存放所有的逻辑门交互行为，若逻辑门的交互端口较多，可为每一个逻辑门建立一张逻辑门端口映射表，表中说明逻辑门编号、源端口、目的端口、状态事件类型、数据流向。

2.2 逻辑门转换规则

在SEFT的逻辑门[9]中，状态不能和事件一样触发逻辑门输出的发生，但是状态可以允许或者禁止逻辑门输出的发生。当所有的卫式条件都为真时，逻辑门才能触发。为了反映状态和事件之间的区别，所有逻辑门的输入和输出都标识了状态和事件端口类型。引入符号<表示先后次序关系，事件类型用E表示，状态类型用S表示。对SEFT的逻辑门类型及其转换规则描述如下：

(1)状态与门(State-AND Gate)：具有一个状态类型的输出和一个或者多个状态类型的输入。它所表示的语义是当所有的输入表达式都满足时，输出状态才会为真。其中输出状态S唯一，输入状态的个数n是任意的，且所有输入的顺序是可交互换的，其转换规则为S=[S1∧S2∧…∧Sn]。

(2)事件状态混合与门(Event/state-AND Gate)：具有一个事件E1输入和n个状态(S1…Sn)输入，输出为事件类型，通常第一个输入是事件类型。该逻辑门的语义为当输入事件触发，并且输入的状态表达式都满足时，输出事件被触发。其转换规则为E=[S1∧S2∧…∧Sn]

(3)状态或门(State-OR Gate)：具有一个状态类型的输出和一个或者多个状态类型的输入。它的语义为当一个或者多个输入表达式得到满足时，输出状态为真。其中输入的状态个数n是任意的，且所有输入状态的顺序是可交换的。其转换规则为S=[S1∨S2∨…∨Sn]。

(4)优先与门(Priority-AND Gate)：具有事件类型的输出和一个或者多个事件类型的输入。它的语义为当输入事件以从左到右的顺序依次发生时，输出事件被触发。其转换规则为E=E1

2.3 顺序逻辑转换规则

通过端口映射表和逻辑门转换规则可以获得由构件状态和事件组成的全局逻辑表达式。对布尔逻辑规则进行扩展，提出顺序逻辑转换规则[10-13]，对全局逻辑表达式进行化简，获得引起系统失效的最小割序集。

分配规则：

交换规则：

E1∨E2⟺E2∨E1

最小化规则：

S1∨S2ifS1⊆S2⟺S1

接下来对分配规则(S1∨S2)

用α,β,γ表示失效状态或事件，所有事件和状态构成的非空集合为Ω，α,β,γ∈Ω，t(α)表示事件或状态的发生时间，若t(α)

σ定义了一个从Ω到{0,1}的映射，其含义是：如果事件A未在规定的时间区间[0,T]内失效，不管以后其失效与否，都认为其真值为0；反之为1。

(1)当t(α)

(2)任取2个大于T，也容易得到等号两边赋值均为0；

(3)任取一个大于T，考虑6种情形：

①0≤t(γ)≤t(β)≤T

②0≤t(β)≤t(γ)≤T

③0≤t(α)≤t(γ)≤T

④0≤t(γ)≤t(α)≤T

⑤0≤t(α)≤t(β)≤T

⑥0≤t(β)≤t(α)≤T

通过证明可得，左右两边赋值均相同，且无永真式或永假式。满足等价性定理。

其余顺序逻辑转换规则，同理可证。

3 实例验证

图1给出一个火灾防护系统的SEFT定性分析实例。顶层事件表示火灾防护系统的失效，PAND门的输出表示检测到火灾，OR2的输出表示喷淋系统失效。该SEFT所描述的危害为：当感烟传感器和感温传感器都相继检测到火灾，但是喷淋系统失效，最终导致火灾发生。

该系统含有7个构件，分别是感烟传感器SD1和SD2，感温传感器HD，温度传感器TS，喷嘴N1和N2，水泵P。另外，含有6个逻辑门，分别为AND3，PAND，OR2，OR1，AND1，AND2。下面将逐步介绍最小割序集的生成过程。

图1 火灾防护系统

第一步：对SEFT的所有逻辑门和组件进行编号，见表1和表2。

表1 组件编号表

表2 逻辑门编号表

第二步：为每个逻辑门和组件建立端口映射表，见表3和表4。

表3 组件端口映射表

表4 逻辑门端口映射表

第三步：将逻辑门转换成逻辑表达式。

第四步：结合端口映射表，自上到下转换成系统失效的顺序逻辑表达式，并根据顺序逻辑转换规则进行化简。

G1out1=(G1in2

第五步：导致系统失效的最小割序集为：

P.S<(SD1.smokedetect<(TS.S

P.S<(SD2.smokedetect<(TS.S

(N1.S∧N2.S)<(SD1.smokedetect<(TS.S

(N1.S∧N2.S)<(SD2.smokedetect<(TS.S

4 评价结果及分析

为了分析基于顺序逻辑SEFT定性分析方法的可行性、可靠性及优缺点，采用基于接口自动机的软件失效行为安全性分析方法[13-14]对该火灾防护系统进行定性分析，评价结果如下所示：

(SD1.smokedetect

(SD1.smokedetect

(SD2.smokedetect

(SD2.smokedetect

基于接口自动机的定性分析方法仅能获得基本事件的失效序列，如上述割序集(SD.smokedetect

5 结束语

针对现有的SEFT定性分析方法中未能体现状态与事件的顺序逻辑关系问题，提出了基于顺序逻辑的状态事件故障树定性分析模型。通过分析构件内部时序活动对系统失效的影响，将构件与外界交互的状态或事件记为可能对系统失效产生影响的候选事件或状态，符合客观实际。同时，定义逻辑门的转换规则，获得由构件状态和事件组成的全局逻辑表达式，根据顺序逻辑规则化简得到最小割序集。

实验结果表明，该方法不仅可以获得导致系统失效的最小割序集，而且可以反映事件和状态之间的优先关系，验证了方法的可行性、可靠性，为SEFT的定性分析方法提供了新思路。

[1] Kaiser B. State event trees: a safety and reliability analysis techniqure for software controlled systems[D].Kaiserslautern:University of Kaiserslautern,2007.

[2] 刘文彬.基于模块化思想的动态故障树分析方法研究[D].南京:南京理工大学,2009.

[3] 郭 勇.基于构件的软件系统的可靠性评估方法研究[D].哈尔滨:哈尔滨工业大学,2013.

[4] 刘 东.空间信息处理系统可靠性设计与分析关键技术研究[D].长沙:国防科学技术大学,2008.

[5] Roth M R,Liggesmeyer P.Qualitative analysis of state/event fault trees for supporting the certification process of software-intensive systems[C]//IEEE international symposium on software reliability engineering workshops.[s.l.]:IEEE,2013:353-358.

[6] Roth M,Hartoyo A,Liggesmeyer P.Efficient reachability gr-aph development for qualitive analysis of state/event fault trees[C]//IEEE international symposium on software reliability engineering workshops.[s.l.]:IEEE,2015:144-151.

[7] 徐丙凤.构件化嵌入式软件安全性分析方法研究[D].南京:南京航空航天大学,2014.

[8] Roth M,Liggesmeyer P.Sequential logic for state/event fault trees:a methodology to support the failure modeling of cyber physical systems[C]//International conference on computer safety,reliability,and security.[s.l.]:Springer International Publishing,2015:121-132.

[9] 李彦锋.复杂系统动态故障树分析的新方法及其应用研究[D].成都:电子科技大学,2013.

[10] Guck D,Han T,Katoen J P,et al.Quantitative timed analysis of interactive Markov chains[C]//NASA formal methods symposium.[s.l.]:[s.n.],2012:8-23.

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

[12] Tang Z,Dugan J B.Minimal cut set/sequence generation for dynamic fault trees[C]//Annual symposium on reliability and maintainability.Charlottesville,USA:IEEE,2004:207-213.

[13] 覃庆努.复杂系统可靠性建模、分析和综合评价方法研究[D].北京:北京交通大学,2012.

[14] Boudali H,Crouzen P 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.

Qualitative Analysis Model of State/Event Fault Tree with Sequential Logic

FAN Ya-qiong，CHEN Hai-yan

(Department of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 210016,China)

In order to overcome the shortcomings of reflecting the relationship between component state and sequential logic in failure system for State/Event Fault Tree (SEFT) qualitative analysis method,a qualitative analysis model of state event fault tree based on sequential logic is proposed.It defines transition rule of logic gate to Boolean logic to define the order of state and event by establishment of the port mapping table of components and logic gates,and gets the sequence of state events (minimum cut sequence set) that leads to system failure according to sequential logic transformation rules to solve the problem of logic order of state and event for system failure.In order to verify the validity and feasibility of the proposed model,a fire protection system has been established as an example of object for verification experiment.It is indicated that the cut order set can reflect the sequential logic relation between the failure event and the state.The feasibility of this model has been verified,which is consistent with the objective reality.Therefore,a new effective approach is provided for the qualitative analysis of SEFT.

sequential logic;port mapping table;minimum cut sequence set;conversion rules;qualitative analysis

2016-08-13

2016-11-23 网络出版时间：2017-07-05

国家“十三五”重点基础科研项目(JCKY2016206B001)；江苏省六大人才高峰项目(XXRJ-004)；软件新技术与产业化协同创新中心资助项目

范亚琼(1990-)，女，硕士研究生，研究方向为软件工程、系统建模与仿真;陈海燕，讲师，研究方向为数据挖掘、民航信息化等。

http://kns.cnki.net/kcms/detail/61.1450.TP.20170705.1650.032.html

TP311

A

1673-629X(2017)08-0012-04

10.3969/j.issn.1673-629X.2017.08.003