2015, Vol. 26
2. 计算机软件新技术国家重点实验室南京大学, 江苏 南京 210023 ;
3. 南京航空航天大学 航天学院, 江苏 南京 210016
2. State Key Laboratory for Novel Software Technology Nanjing University, Nanjing 210023, China;
3. College of Astronautics, Nanjing University of Aeronautics and Astronautics, Nanjing 210016, China
嵌入式实时系统已在航空航天、核工业、公共交通等安全关键领域中得到广泛应用,其系统失效将会导致财产的重大损失、环境的破坏甚至人员的伤亡[1].因此,对嵌入式实时系统中可能出现的危险失效状况进行安全相关时间特性(如危险失效的平均时间[2]、故障间隔时间[3]等)的建模与分析,已成为现代复杂嵌入式系统安全性保障的重要方法和研究热点.状态事件故障树(state/event fault tree,简称SEFT)[4]是一种结合了故障树元素与状态机语义的系统行为安全性建模方法,其模型中的顶层事件表示系统的失效结果,并通过系统基本构件与不同类型逻辑门操作的组合来刻画系统失效结果发生的因果层次关系.SEFT适合于对当前安全关键领域中所应用的大多数分布式构件化嵌入式系统的安全行为进行建模[5].
对SEFT顶层事件发生的时间进行定量分析,是获得系统失效时间参数的一种有效途径.但由于SEFT模型中尚缺乏严格语义,为分析其时间特性,需要给出其准确语义.目前,对SEFT进行严格的语义描述已有一些相关研究工作,如,文献[6, 7]采用传统的Petri Net对SEFT进行语义描述,但Petri Net缺少描述SEFT构件之间消息交互的形式语义,使得对SEFT中的构件和逻辑门进行描述之后仍需要专业人员进行手动合并和修改才能够形成完整的分析模型;并且在形成SEFT完整语义模型的过程中,难以进行状态空间的约简.此外,由于SEFT具备构件化特征以及描述系统动态行为的能力,因此也很难使用诸如二叉决策图(binary decision diagrams,简称BDD)[8]等之类的技术对其进行准确描述.本文工作给出了一种基于交互马尔可夫链(interactive Markov chain,简称IMC)的SEFT时间特性分析方法,能够给出符合SEFT模型特征的形式语义模型并进行SEFT时间特性的自动定量分析.考虑到SEFT顶层事件发生的平均时间即该失效在系统中出现的平均时间,该时间特性是评估系统安全性的一项非常重要的指标[9],因此,本文主要针对SEFT中顶层事件发生的平均时间分析展开论述.
本文第1节对SEFT的建模元素进行详细描述,并给出一个SEFT的建模实例.第2节提出一个新的接口交互马尔可夫链模型(interface interactive Markov chain,简称Interface-IMC).该模型将IMC中的交互动作精化为输入、输出动作,并给出并行组合以及弱互模拟的语义.第3节采用Interface-IMC对SEFT构件行为和逻辑门的语义进行建模.第4节通过并行组合方式得到SEFT的全局行为语义模型,在组合的过程中,采用弱互模拟对状态空间进行约简,并设计SEFT顶层事件发生的平均时间分析方法.第5节分别给出飞机着陆雷达控制系统和喷淋防火系统的SEFT建模以及时间特性分析的实例研究.第6节进行相关工作的比较.最后,对全文进行总结并阐述未来的工作.
1 状态事件故障树本节概要描述了状态事件故障树的基本建模元素,并给出了一个飞机着陆雷达控制系统的状态事件故障树应用实例.
状态事件故障树(SEFT)[6]模型中包含了状态机元素和故障树元素,其在传统故障树的基础上进一步区分了系统行为状态和事件,且引入了显式的事件符号和因果边用于描述构件状态的转换以及构件之间失效的因果关系.在SEFT中,系统各构件通过多种类型的逻辑门进行连接,通过构件行为的描述以及构件之间的关系描述系统中失效发生的因果链.其基本建模元素如图 1所示,包括:
(a) 构件(component):表示具有相对独立功能的软件或硬件实体,通过端口(port)与其他构件进行连接.
(b) 端口(port):表示SEFT中构件以及逻辑门之间的交互,包括事件的输入/输出端口、状态的输入/输出端口这4种类型.
(c) 逻辑门(gate):表示多个构件失效时相互之间影响的逻辑层次关系.其中,
(1) AND门表示所有输入失效都发生时输出失效才会发生;
(2) OR门表示所有输入当中有一个失效发生时输出失效就会发生;
(3) VOTING门表示当前输入当中的某几个失效发生时输出失效发生;
(4) PAND门表示当前输入以从左到右的顺序全部发生时输出失效才会发生.
(d) 事件(event):表示一种原子事件,即,无时间延迟的触发动作.
(e) 状态(state):表示构件中相关变量的抽象等价类集合.在每个时间点,系统应处于有限状态集合中的某个状态,并且在一定的时间区间内状态不变.如:飞机的高度是相关变量,该变量具有{too low, acceptable,too high}这3种状态,在每个时间点,系统处于这3个状态中的一个,并且在某个时间范围内都处于该状态.
(f) 边(edge):表示状态之间转换,包含两种类型:
(1) 一种是时序边,其停留时间根据指数分布随机改变;
(2) 另一种是因果边,即事件触发引起状态改变.
 | Fig. 1 Main modeling elements of SEFT图 1 SEFT的主要建模元素 |
图 2(a)描述了一个构件内部的时序边,系统在S1状态的停留时间服从参数为l指数分布,之后转换到S2状态.图 2(b)描述了系统中C1和C2两个构件之间的因果边,C1构件中事件E1的发生触发构件C2中E1的发生.
 | Fig. 2 Different ways of event occurrence图 2 事件发生的不同方式 |
我们可以使用SEFT模型对安全关键系统中导致某个失效结果的原因建立起失效因果关系链.图 3给出了一个飞机着陆雷达控制系统(aircraft radar landing control system,简称ARLCS)的SEFT失效模型示例.该例中的失效结果为“飞机高度低于指定着陆高度时着陆轮却未放下”.该系统中主要包含3个构件,分别是着陆轮控制器(landing wheel controller)、雷达系统接口(radar interface)、雷达数据验证器(radar data validator):
· 着陆轮控制器用于控制着陆轮收起或者放下,当飞机高度小于100m或在地面时,着陆轮必须放下.
· 雷达接口负责提供当前飞机所处高度的数据.
· 雷达数据验证器用于监控雷达接口是否正常工作以及所提供的数据是否正确,当发现雷达接口故障时发出预警.
该SEFT模型通过两个AND门以自底向上的方式连接3个构件,描述了该失效结果发生的因果关系链.即,在飞机的着陆轮收起的情况下,当飞机的高度小于100m时,雷达接口出现故障且雷达数据验证器未能正常预警,出现着陆轮放不下的情形.其中,各构件的内部行为通过有限状态机进行描述,该有限状态机同时描述构件的动作与时间行为.如,雷达系统接口到达failed状态的时间服从参数为l的指数分布.
 | Fig. 3 SEFT example of ARLCS图 3 ARLCS的SEFT示例 |
如前所述,SEFT模型缺乏严格语义,难以直接对其进行分析.因此,本节建立了符合SEFT特征的形式语义模型,用于严格定义SEFT的语义.通过将交互马尔可夫链(IMC)[10, 11]的交互动作语义精化为输入、输出动作,本节中提出了一种接口交互马尔可夫链(Interface-IMC)模型,定义了并行组合操作用于描述构件系统中的组合行为语义,并给出了用于对组合过程中的状态空间进行约简的弱互模拟操作定义.
2.1Interface-IMC模型考虑到SEFT构件内部采用有限状态机同时描述功能与时间特性,通过端口接收输入或进行输出与外部构件以及逻辑门进行交互,因而,SEFT的构件和逻辑门可以看作是通过接收特定的输入信号或产生输出信号与环境进行交互.IMC具有同时描述构件行为和时间特性的能力,并且提供了并行分析框架,适合描述SEFT中构件与逻辑门的行为特性.但IMC中缺少输入、输出动作的概念,难以准确描述SEFT中构件之间的交互特征.为了尽可能地使所建立的模型与SEFT中构件和逻辑门的行为语义相一致,本文对IMC中的交互动作进行精化,即,将IMC中的动作区分为输入、输出动作,并明确地标识出在当前状态上哪些输入动作是可接受的,而在当前状态没有标识的动作则视为不可接受的,从而建立起一个Interface-IMC.
具体的Interface-IMC的形式定义如下:
定义1. 一个接口交互马尔可夫链P是一个五元组(S,s0,A,®,®M),其中,
· S是状态集合.
· s0是初始状态.
· A是动作集,其中,A=(AI,AO,Aint),AI为输入动作集,AO为输出动作集,Aint为内部动作集,记AV=AIÈAO为P的可见动作集,Aint为P的不可见动作集.
· ®是交互转换集合.通常将(s,a,s¢)ή记作
· ®MÍSx¡>0xS是马尔可夫转换集合.通常将(s,l,s¢)ήM记作
,表示s到s¢转换发生的时间服从参数为l的指数分布,l称为转换率.
图 4以图形化的方式描述了两个Interface-IMC P和Q的直观语义.P和Q中存在两种类型的转换:
(1) 实线箭头表示采用动作进行标记的交互转换;
(2) 虚线箭头表示采用时间参数进行标记的马尔可夫转换.
由定义1,图 4(a)中:Interface-IMC P状态集为S={S1,S2,S3},初始状态为S1;动作集A中,AI=Æ,AO={a},Aint=Æ;交互转换集®={(S2,a!,S3)};马尔可夫转换集®M={(S1,l,S2)}.
该Interface-IMC直观语义为:系统从初始状态S1出发,经过一个停留时间t=T(l)转换到S2状态,t服从参数为l的指数分布;然后,通过产生一个输出动作a转换到S3状态.图 4(b)中的状态K2则是通过接收输入动作a转换到K4状态.
 | Fig. 4 Two examples of Interface-IMC图 4 Interface-IMC的两个示例 |
并行组合操作让使用子构件的本地行为模型来构建构件系统的全局行为模型成为可能[12].在并行组合的过程中,两个Interface-IMC之间会存在交互同步,即,其中一个Interface-IMC输出动作a,而另一个Interface-IMC正好需要接收该动作.不妨设有两个构件P和Q的Interface-IMC模型,记P和Q的共享动作集:
即,一个Interface-IMC的输出动作是另一个Interface-IMC的输入动作,则两个Interface-IMC在执行该动作时需同步,且此相同动作的集合就是共享动作集shared(P,Q).如图 4中,P和Q的共享动作集为shared(P,Q)={a}. P||Q可以描述如下:
(1) 如果动作不需要进行同步,则P和Q可以单独进行状态转换,即,如果P执行任何动作并转换为P¢,则在并行语义中也存在相同的行为.即,P||Q可以转换为P¢||Q.
(2) 如果交互转换的动作需要进行同步,则P和Q需要同时执行该操作,即,P||Q可以转换为P¢||Q¢.此时,当P(或Q)的输出动作和Q(或P)输入动作同步时,将产生一个并行组合P||Q中的内部动作.
Interface-IMC的“并行组合”定义如下:
定义2. Ρ和Q为两个Interface-IMC,并行组合P||Q为
其中,
根据以上并行组合规则,图 4(a)中的P和图 4(b)中的Q并行组合结果为图 5(a)中的P||Q.
 | Fig. 5 Composition and aggregation of Interface-IMC 图 5 Interface-IMC的组合及聚合 |
由于两个Interface-IMC并行组合后的状态空间大小与它们的状态空间数的乘积成正比,因此在多个Interface-IMC并行组合的过程中可能会出现状态空间爆炸的情况,需要采用合适的状态空间约简技术.本文采用Interface-IMC中状态等价的方法,通过将等价状态聚合,得到一个保持原模型行为语义但规模更小的模型.具体而言,我们采用类似IMC中弱互模拟[10]的概念进行Interface-IMC状态空间等价类的划分,然后再采用聚合操作进行状态空间的约简,即,将同一等价类中的状态合并为一个状态.与IMC不同的是,Interface-IMC通过将IMC的交互动作精化为输入、输出动作,且明确地标识了状态上所允许的动作集,不允许的动作是不作标识的,这使得在并行组合过程中可以更有效地生成Interface-IMC模型的状态空间.在Interface-IMC中,两个状态视为弱互模拟等价,则要求所有这两个状态具有相同的可观察行为,且表现相同的性能特性.
设P是一个Interface-IMC,s,s¢ÎS是P中的状态,若存在一个转换序列:
则记为
若s状态不存在内部转换或输出转换,则称该状态是稳态,即,无法通过瞬时转换到达另一状态.此外,从状态s到状态集C的累积转换率标识从状态s到达状态集C中所有状态的转换率之和,定义为
其中,{|…|}标记转换率的多个集合.集合Cint={s¢|$sÎC.s¢Þs}包含所有通过弱转换(Þ)到达C集合的状态.
Interface-IMC“弱互模拟”的定义如下:
定义3. 设P=áS,s0,A,®,®Mñ是一个Interface-IMC,R是S上的一个等价关系,当且仅当对于所有的(s,t)ÎR, aÎA有以下条件成立时,R是一个弱互模拟关系:
· 
且(s¢,t¢)ÎR;
· 对于R上的所有等价类C,若sÞs¢且s¢是稳态,则存在t¢ÎS,使得tÞt¢,t¢是稳态且gM(s¢,Cint)=gM(t¢,Cint).
若P和Q包含在某些弱互模拟关系当中,即,P和Q是弱互模拟的,记作P≈Q.Interface-IMC的弱互模拟定义对IMC弱互模拟定义进行了精化,将交互动作精化为输入、输出动作.对Interface-IMC进行弱互模拟等价类划分之后,可以通过聚合操作得到一个与原Interface-IMC弱互模拟等价但规模更小的模型,即,将相同等价类中的状态合并为同一状态.图 5(b)给出了针对图 5(a)中的Interface-IMC应用弱互模拟操作进行等价类划分并且进行状态空间聚合后的结果.可以看出:图 5(a)中的状态(S1,K2),(S2,K1),(S2,K2),(S3,K3)是弱互模拟等价的,这4个状态都是经过一个转换时间服从参数为l的指数分布到达(S3,K4)状态,在图 5(b)中,这4个状态聚合为T2状态.
定理1. P1和P2是两个具有相同动作集的Interface-IMC,P3是一个可以与P1和P2进行并行组合的Interface- IMC,则,
(1) P1≈P2,则P1||P3≈P2||P3;
(2) P1≈P2,则P3||P1≈P3||P2.
定理1的证明见附录.定理1表明,本文定义的弱互模拟针对并行组合操作是可替换的.该定理保证了可以利用弱互模拟化简之后的构件与其他构件进行并行组合,且最终的并行组合结果与不进行任何状态约简的并行组合结果是弱互模拟的.这样,在多个Interface-IMC的并行组合过程中,就可以采用弱互模拟操作来减少模型的规模.
3SEFT的形式化语义描述对SEFT进行形式语义描述是分析其时间特性的基础,本节采用上一节中所建立的Interface-IMC模型对SEFT的构件与逻辑门进行严格的语义描述.
3.1SEFT构件的语义如第1节中所述,SEFT中含有两种转换边:一种是时序转换边;一种是因果转换边.对于时序转换边,由于描述的是构件内部状态转换关系,可以采用Interface-IMC中的交互转换对其进行表示.对于随机延时的时序转换边,其表达的是系统经过一个指数时间的随机延迟转换到下一状态,可采用Interface-IMC中的马尔可夫转换进行表示;对于表示构件之间事件触发关系的因果转换边,存在触发事件与被触发事件之间的关系,可以使用Interface-IMC输入/输出动作的同步对因果转换边进行描述.
综上,采用Interface-IMC描述SEFT构件语义的方法如下:
(1) 构件的状态采用Interface-IMC的状态描述;
(2) 构件的事件采用Interface-IMC的动作描述;
(3) 构件内部状态通过时序边相连的情形,可采用Interface-IMC中的交互转换来表示;
(4) 构件之间的因果边采用Interface-IMC之间输出与输入动作发送与接收的同步,对动作触发进行 描述;
(5) 状态和事件端口所表示的消息交互,可用Interface-IMC中消息的输入、输出类型对其进行描述.
考虑到本文的主要工作是对SEFT进行时间特性分析,因此在描述时序边语义时,对于不参与其他构件交互的构件内部状态的时序边上的信息,只保留对应的时间参数,而不需要保留事件信息.此外,因果边采用Interface-IMC之间的输出与输入动作的发送与接收进行描述,即,两个构件对于同一个动作同步,一个构件发送消息,另一个构件需要接收相同的消息.如图 2(b)中的因果边的语义可用Interface-IMC描述为:构件C1行为表示为
C2行为表示为
通过E1动作的同步,就可以描述构件事件发生的因果关系,即,构件C1发送E1消息,构件C2接收到E1消息后,则从S1状态转换到S2状态.
下面使用Interface-IMC对SEFT逻辑门进行语义描述.SEFT逻辑门上所有的状态接口输入或者事件接口输入都来自构件或其他逻辑门的输出动作,下面给出每一种逻辑门的语义定义,其中,每一种逻辑门的语义(记为
)是一个函数,以若干动作作为输入,输出为相应的Interface-IMC:
(1) AND门
图 6(a)给出了两输入AND门(AND,2)的语义,即,函数
以AND门的输出以及两个输入信号作为参数.当AND门接收到两个输入信号时才会触发;
(2) OR门
图 6(b)给出了两输入OR门(OR,2)的语义,即,函数
以OR门的输出和两个输入信号为参数.当OR门接收到其中一个输入信号时,OR门被触发;
(3) PAND门
图 6(c)给出了两输入PAND门(PAND,2)的语义,即,函数
以PAND门的输出和两个输入作为参数.当PAND门接收到以从左到右的顺序发生的两个输入信号时被触发;
(4) VOTING门
图 6(d)给出了2/3 VOTING门(VOTING,3,2)的语义,即,函数
以VOTING门的输出和3个输入信号为参数.当VOTING门的3个输入信号中的两个两个输入信号被触发时, VOTING门被触发.
 | Fig. 6 Semantic model of SEFT logic gate based on Interface-IMC 图 6 基于Interface-IMC的SEFT逻辑门语义模型 |
在得到SEFT构件与逻辑门的Interface-IMC语义模型之后,我们就可以通过并行组合SEFT中的构件和逻辑门的语义模型得到整个SEFT的行为语义模型,并基于此进行时间特性分析.
4SEFT的时间特性分析本节介绍SEFT的时间特性分析方法.这里假定SEFT模型是合法模型(注:判断SEFT是否合法的具体步骤见文献[6]),并且SEFT各构件中的失效参数都已通过统计计算方法获得.以下首先给出Interface-IMC的并行组合状态空间约简方法的说明及相应算法,然后给出了SEFT顶层事件发生的平均时间的详细分析方法及相应的原型分析工具架构.
4.1 接口交互马尔可夫链的约简Interface-IMC并行组合过程中可能会出现状态空间爆炸的情形,下面对本文所采用的状态空间约简技术进行详细说明.根据第2.3节中的定理1可知,Interface-IMC的弱互模拟针对并行组合具有可替换性,因此可以使用聚合之后的构件代替原构件继续与其他构件进行并行组合操作.因此在Interface-IMC组合过程中,每进行两个Interface-IMC的组合后,都可采用Interface-IMC的弱互模拟技术对所生成的Interface-IMC进行状态空间约简操作,约简状态空间之后再进行下一次组合.这样,就可以在组合的过程中减少所生成的状态.具体而言,进行状态空间约简分为两个步骤:
· 首先,划分组合模型中的状态空间的等价类;
· 其次,根据所划分的等价类对模型进行聚合操作.
其中,划分组合模型中的状态空间的等价类是该步骤的关键,下面着重对这部分进行介绍.
目前已经存在一些采用弱互模拟操作对模型进行约简的算法.比如,文献[13]提出了一种针对IMC计算最小模型的算法,但是只能计算无环模型,而系统行为模型中往往存在环,所以难以直接采用这种方法.文献[14]的CADP(construction and analysis of distributed processes)工具集中的BCG_min可用于对标记转移系统(label transition system,简称LTS)的相关模型进行约简,但难以直接将该方法应用到接口交互马尔可夫链模型中进行状态空间的约简.文献[10]给出了基于IMC的弱互模拟等价类划分方法,能够适用于计算存在环的IMC模型.而Interface-IMC将IMC的交互动作精化为输入、输出动作,所以在对Interface-IMC的状态空间进行弱互模拟等价类划分的过程中,与IMC中稳态[10]的定义不同的是,Interface-IMC的稳态是指不存在输出转换和内部转换的状态.此外,采用交互动作对Interface-IMC的状态空间进行等价类划分时,需严格区分动作的输入、输出类型.
Interface-IMC的弱互模拟等价类划分算法如算法1所示.下面首先给出算法中出现的一些公式和符号的相应说明.
若Interface-IMC中的P状态经过一系列的内部动作演化可以到达稳定状态则记为
当且仅当
为任意输出动作;否则,记为
在算法中将用到函数gO:SxActx2Sa{true,false},gO(P,a,C)为真当且仅当P可以通过
演化到状态集C中,
其中,a可以是输入动作或输出动作.
该算法的思想是:首先,根据Interface-IMC状态空间中所有状态是否为稳态对状态空间进行等价类划分;再分别针对每个等价类利用动作集Act对状态空间进行等价类划分;此外,对于稳态等价类中的状态,进一步根据时间参数特性对状态进行划分.如此迭代,直到所有的动作都已用于进行状态空间的划分,最后得到一个划分成若干个等价类的状态空间.
算法1. Computing weak bisimilarity classes.
Rest(X,C)=X-{PÎY|YÎM_Spread(X,C)}.
Input: Interface-IMC Interface-IMCR=(S,s0,A,®,®M).
Output: TC_PartÈTD_Part. //Weak bisimilarity classes of Interface-IMCR
Function: Computing weak bisimilarity classes of Interface-IMCR.
Substitute all internal actions of Interface-IMCwith t;
Spl:=Actx{TC_PartÈTD_Part}.
repeat
choose (a,C) in Spl;
Old:=TC_PartÈTD_Part;
TC_Part:=IRefine{TC_Part,a,C}; //partition TC_Part by action a
TD_Part:=IRefine{TD_Part,a,C}; //partition TD_Part by action a
TC_Part:=IM_Refine{TC_Part,C}; //partition TC_Part by Markov transition
New:=(TD_PartÈTC_Part)-Old;
Spl:=(Spl-{(a,C)})È(ActxNew); //update Spl
until Spl is empty;
return TC_PartÈTD_Part.
算法主要分为两个部分:
第1部分是初始化操作,计算能够通过内部动作到达稳态的所有状态集TC_Part以及通过内部动作无法到达稳态的所有状态集TD_Part,根据该计算结果修改Spl,即,Actx{TC_PartÈTD_Part}.
第2部分是算法的主体部分,先从Spl中取出一个动作,使用该分类动作对TC_Part和TD_Part划分等价类;针对TC_Part进一步采用时间参数特性对其状态进行等价类划分,且根据新增等价类添加相应的分类动作到Spl中,当Spl为空时循环结束.
在整个算法的处理流程中,算法的第1部分是初始化操作,根据文献[15]的分析计算可知,其时间复杂度为O(n2.376).第2部分在最坏情况下需执行n次(即,每个划分中只含有一个状态),根据文献[10, 16]可知,该过程的时间复杂度为O(nxm),其中,n为Interface-IMC的状态数,m为马尔可夫转换数和经过内部传递闭包计算之后的交互转换数之和,m最大值为nx(n-1).因此,该算法的时间复杂度为O(n3).
在得到了状态空间的等价类划分之后,我们就可以使用聚合方法对Interface-IMC模型中的等价类进行约简操作,即,分别对模型中的每个等价类进行处理,将处于同一个等价类的状态合并为一个状态,并构造Interface-IMC模型中其他状态到该新状态的概率转换以及动作转换.经过聚合操作之后,可以得到一个状态空间更小且与原来的模型弱互模拟的Interface-IMC.例如,针对图 5(a)中的Interface-IMC,可以使用该算法步骤进行等价类的划分,得到的等价类为{{(S1,K1)},{(S1,K2), (S2,K1),(S3,K3)},{(S2,K2),(S3,K4)},{(S3,K5)}},进行聚合操作之后得到如图 5(b)所示的Interface-IMC.
4.2SEFT时间特性计算采用Interface-IMC精确描述SEFT的语义模型之后,SEFT的顶层事件在Interface-IMC中表示为一个输出动作,因此,SEFT顶层事件发生的平均时间即为相应的Interface-IMC模型中顶层事件对应的输出动作发生时间的期望值.由Interface-IMC交互动作的定义可知,输出动作是由构件自身控制的,通常可认为输出动作的发生不产生时间延迟,因此,对该输出动作发生的时间期望值进行计算可进一步转换为计算该输出动作的出发状态到达时间期望值.在本文中,为了方便SEFT平均时间的计算,采用了一个IMC的分析工具IMCA(interactive Markov chains analyzer)[17],可用于计算交互马尔可夫链(IMC)中从初始状态到达目标状态时间的最大和最小期望值.
如前文所述,为了准确地描述SEFT构件之间的消息交互,Interface-IMC将IMC的交互动作精化为输入和输出动作,可以表达构件以及逻辑门之间的并行组合语义,并得到SEFT的完整语义模型.考虑到对SEFT顶层事件的平均时间的计算而言,在Interface-IMC中动作的输入、输出类型其实并不影响时间期望值的计算结果,因此,在Interface-IMC中计算到达特定状态的时间期望值时,可将输入、输出动作都处理为一类相同的IMC的交互动作.这样就可以很方便地使用IMCA来计算Interface-IMC的平均时间特性.
此外,从SEFT构件和逻辑门的形式语义模型的并行组合中可以得到,除了描述SEFT顶层事件语义的输出动作未形成内部动作以外,其他所有构件和逻辑门的输入动作都经过同步成为内部动作,经过弱互模拟操作后被约简.因此,在最终描述SEFT完整语义的Interface-IMC中,事实上只存在若干个马尔可夫转换和一个输出动作转换.令描述SEFT完整语义的Interface-IMC P=(S,s0,A,®,®M),SEFT顶层事件所对应的输出动作的出发状态为s¢.在IMCA中,其接受的输入文件中包含了马尔可夫转换与交互转换以及所分析的初始状态INITIALS和目标状态GOALS.我们可以s0为初始状态INITIALS,以s¢为目标状态GOALS,根据P中的转换关系构造IMCA可接受模型文件.IMCA计算出的INITIALS到达GOALS时间的最大和最小期望值结果可以对应到SEFT中,即为顶层事件发生的最大和最小平均时间,也就是在系统中各构件的失效参数已知的情况下,系统中特定失效发生的最大和最小平均时间.这个结果可以为评估系统的安全性提供参考.对于安全关键系统而言,我们通常会采用最小平均时间作为评估系统安全性的标准.
综上所述,可对本文所提出的SEFT时间特性分析方法的实现模型进行概括,具体的处理流程如图 7所示:
· 首先,对SEFT进行形式语义描述,创建所有逻辑门和构件的Interface-IMC模型;
· 其次,针对所得到的Interface-IMC集合进行并行组合操作,得到SEFT的完整语义模型,并且在组合的过程中利用弱互模拟操作进行状态空间的约简;
· 最后,对SEFT的完整语义模型采用时间特性分析工具IMCA(interactive Markov chains analyzer)[18]对顶层事件发生时间的期望值进行计算.
由于该处理过程中每个步骤都是可终止的,因此本文的方法是可终止的.
在CSFATA中,上述主要模块的功能是基于Eclipse平台开发的,已经完成其核心功能的设计与实现,目前正在进行与相关工具的集成和更多的实例研究.
 | Fig. 7 Implementation flow of SEFT time property analysis图 7 SEFT时间特性分析的实现流程 |
在上述工作的基础上,我们设计了一个相应的系统失效时间建模与分析原型工具(critical system failure time modeling & analyzer,简称CSFATA).该工具的系统架构如图 8所示,包括4个主要的子模块:
· 用户接口模块(user interface)用于与用户进行交互,接受用户的输入操作;
· Interface-IMC模型建立模块(Interface-IMC generator)用于对SEFT的XML文件进行解析,并创建Interface-IMC模型;
· 核心算法处理模块(kernel algorithm processor)用于完成并行组合以及状态空间的约简,并利用已有的分析工具IMCA对最终的接口交互马尔可夫链模型进行时间期望值计算;
· 结果显示模块(result displayer)用于对计算结果进行输出显示.
 | Fig. 8 System architecture of CSFATA图 8 CSFATA的系统架构 |
本节分别采用飞机着陆雷达控制系统和喷淋防火系统的状态事件故障树实例,根据所提出的方法对其顶层事件发生的最大和最小平均时间进行分析.为表述清晰,本文给出了完整的执行过程描述.
5.1 飞机着陆雷达控制系统SEFT实例针对第1节中图 3给出的飞机着陆雷达控制系统(ARLCS)的状态事件故障树模型,使用本文所提出的方法对其顶层事件发生的最大和最小平均时间进行分析.
首先,对于图 3中的SEFT,采用Interface-IMC给出其严格语义.该SEFT中一共包含3个构件与两个逻辑门,采用Interface-IMC精确描述3个构件与两个逻辑门的语义,如图 9所示.本文根据SEFT中的构件与逻辑门的层次对得到的Interface-IMC进行编号.可以看出,对该SEFT的顶层事件发生的平均时间的分析就转换成计算到达C5中S3状态时间的期望值.
 | Fig. 9 Semantic models of SEFT components and logic gates in example图 9 实例中SEFT构件与逻辑门的语义模型 |
在得到SEFT中构件和逻辑门的Interface-IMC形式语义模型之后,通过对这些Interface-IMCs进行并行组合操作得到SEFT的精确语义模型.该实例中组合的顺序为((C1||C2)||(C3||C4))||C5,每进行一步组合,都采用弱互模拟对组合产生的Interface-IMC状态空间进行约简,并将约简的结果再进行下一次组合.以此类推,形成最终的组合Interface-IMC.
整个并行组合以及约简过程如图 10所示.由于在该实例中f5!是顶层逻辑门的输出,SEFT中的顶层事件发生时间的期望值计算即计算图 10(h)中S0状态到达S3状态的时间期望值.
 | Fig. 10 Composition and aggregation process of the aircraft radar landing control system图 10 飞机着陆雷达控制系统组合聚合过程 |
下面利用IMCA对图 10(h)进行时间期望值的计算.
图 10(h)的IMCA输入文件ARLCS.imc见表 1:初始状态为S0,目标状态为S3,并通过状态与转换描述了整个Interface-IMC.这里,各构件的失效都满足指数分布,具体的失效率参照文献[19]中提供的数据.l和m的取值分别为0.002和0.001,假设时间单位为小时(h).该实例关注对SEFT中顶层事件发生的最大和最小平均时间的分析,即,在SEFT的Interface-IMC语义模型中,从初始状态到目标状态时间的最大和最小期望值.使用IMCA对本文实例进行计算.通过计算,该状态事件故障树中顶层事件发生时间的最大和最小期望值相同,都为1 166h.即,在该系统中各构件发生故障时间参数已知的情形下,顶层事件发生的最大和最小平均时间都为1 166h.其物理含义为:飞机着陆雷达控制系统“飞机高度低于特定值时着陆轮未放下”失效发生的最大和最小平均时间均为1 166h,且该时间值越大,系统能够正常工作的时间就越长.该参数可为评估飞机着陆雷达控制系统的安全性提供参考.
|
Table 1 IMCA input file for the example 表 1 实例的IMCA输入文件 |
图 11给出了一个喷淋防火系统的SEFT失效模型示例.该例中的失效结果为“喷淋防火系统失效”.该系统主要包含3个构件,分别是感烟传感器(smoke detector)、感温传感器(heat detector)、喷淋控制器(sprinkler controller).当感烟传感器或者感温传感器被触发时即进行火灾报警,然后喷淋控制器进行喷淋灭火.该SEFT模型通过一个AND门和一个OR门以自底向上的方式连接3个构件,描述了该失效结果发生的因果关系链.即,当感烟传感器和感温传感器都失效或者喷淋控制器失效时,造成喷淋防火系统失效.系统中各构件的失效都满足指数分布,具体的失效率参照文献[20]中提供的数据,即,感烟传感器的失效率l1=0.002,感温传感器的失效率为l2=0.004,喷淋控制器的失效率为l3=0.000001,这里假设时间单位为小时(h).
 | Fig. 11 SEFT of sprinkler system图 11 喷淋防火系统SEFT |
首先,针对图 11中的SEFT采用Interface-IMC给出其严格语义.该SEFT一共包含3个构件和两个逻辑门,采用Interface-IMC描述3个构件与两个逻辑门的语义如图 12所示.其中,由OR门的语义可以看出,任意一个输入的发生都能触发输出的发生.因此,这里将OR门描述为如图 12(e)所示的两部分,分别与对应的构件进行并行组合.本文根据SEFT中逻辑门的层次对得到的Interface-IMC进行编号.可以看出，对该SEFT的顶层事件发生的平均时间的分析,就转换成计算图 12中从初始状态到达C5和C6中S1状态时间的期望值.在得到SEFT中构件和逻辑门的Interface-IMC的形式语义模型之后,通过对这些Interface-IMCs进行并行组合聚合操作,得到SEFT的形式语义模型.由于OR门的逻辑语义描述分为两部分,因此并行组合也分为两部分,组合顺序根据模型的特征给定,分别为((C1||C3)||C4)||C5和C4||C6.组合聚合过程如图 13所示,由于OR门的存在,最终得到的Interface-IMC模型分别如图 13(f)和图 13(h)所示.由于在该实例中f5!是顶层逻辑门的输出,计算SEFT中的顶层事件发生时间的期望值即计算图 13(f)中S0状态到达S3或者图 13(h)中S0状态到达S1状态的时间期望值.
 | Fig. 12 Semantic models of sprinkler system SEFT components and logic gates图 12 喷淋灭火系统SEFT构件和逻辑门的语义模型 |
 | Fig. 13 Composition and aggregation process of the sprinkler system图 13 喷淋防火系统组合聚合过程 |
下面针对这些模型采用IMCA进行时间特性分析.图 13(f)和图 13(h)的IMCA输入文件sprinkler1.imc和sprinkler2.imc见表 2.
|
|
Table 2 IMCA input file for the sprinkler system example 表 2 喷淋防火实例的IMCA输入文件 |
该实例关注对顶层事件发生的最大和最小平均时间的分析,即,在SEFT的Interface-IMC语义模型中,从初始状态到目标状态时间的最大和最小期望值.使用IMCA对该实例进行计算.通过计算,该状态事件故障树中顶层事件发生时间的最大和最小期望值分别为1 000 000h和583h.即,在该系统中各构件发生故障时间参数已知的情形下,顶层事件发生时间的最大和最小平均时间分别为1 000 000h和583h.其物理含义为:喷淋防火系统“喷淋防火系统失效”发生的最大和最小平均时间分别为1 000 000h和583h.值得注意的是,从上述例子中也可以看出:由于原始数据是指数分布的参数,因此,当原始数据越大,其平均时间就越小.
6 相关工作在嵌入式实时系统开发的过程中获得与系统安全相关的时间特性,是对系统进行安全性评估的依据.目前,在系统失效因果链描述方面,故障树(fault tree,简称FT)[21]已经在工业界广泛应用.但FT无法表达动态系统中的时间依赖以及序列依赖的行为,已有一系列工作对其建模能力进行扩展以支持动态系统以及实时系统的建模,主要包括:动态故障树(dynamic fault tree,简称DFT)[22]在故障树的基础上扩展了动态门用于建模动作序列之间的依赖关系;时序故障树(temporal fault tree,简称TFT)基于连续逻辑[23]、区间时序逻辑[24]等时序逻辑描述系统中的时序关系,并针对TFT进行定性分析,考虑可达性、可满足性等;此外,文献[25]给出了优先与门(PAND)的定义并处理序列依赖的动态行为;文献[26]提出一些新的表达失效之间时间特性的逻辑门,用于表达原因和结果之间的定量时间关系.以上方法都可以表达系统中的失效发生的因果关系链,但是仍缺少描述构件化系统中建模事件顺序以及状态依赖的能力.SEFT[4]将传统故障树元素与状态机元素结合起来,既能表达危害场景发生的因果关系链,又能描述动态系统行为中的时间依赖和序列依赖属性,适用于对构件化嵌入式系统失效因果链进行建模分析.
由于FT,DFT以及SEFT都缺乏形式语义,难以直接对它们进行分析,通常采用具有精确语义的形式模型严格描述其语义再进行分析.文献[27]采用二叉决策图描述FT的语义,在精确定义语义的基础上计算FT中顶层事件发生的概率;文献[28]通过利用广义随机Petri Net对FT进行精确语义描述,并分析其概率特性;文献[29]采用马尔可夫链模型对DFT进行精确的语义描述,并给出定量分析框架.而对于SEFT的定量分析,文献[6]采用Petri Net对其进行形式语义描述,并在此基础上进行顶层事件发生的概率特性分析.但由于Petri Net缺乏描述构件之间消息交互的语义,难以精确描述构件之间的并行组合,因此在使用Petri Net对SEFT进行形式语义描述之后,需要手动对模型进行修改以及合并才能生成完整的SEFT语义模型,且未提供状态空间约简方法,难以有效地自动生成完整的语义模型,因此难以基于该语义模型对状态事件故障树的时间特性进行分析.
在对系统的失效发生的时间特性分析方面,文献[30]利用具有时间依赖的故障树(fault tree with time dependencies,简称FTTD)对失效发生的时间进行定量分析.文献[31]结合FTTD和UML(unified modeling language)状态机图分析从原因的出现到最终失效发生之间所经过的时间间隔.文献[32]针对安全关键实时嵌入式系统中的基于失效依赖的最坏执行时间进行了详细的分析.同时,还存在一些工作对安全关键嵌入式软件的时间特性进行建模分析.文献[33]利用实时接口自动机描述实时系统的构件交互行为模型,并且对给定的实时规约进行验证.文献[34]中给出了一个实例研究,说明如何将一个简单的UML顺序图转换成一系列时间自动机,然后使用时间自动机的相关验证工具进行验证.文献[35]对基于场景的规约进行了时间扩展,用于表示实时系统的时间属性,并生成对应的时间自动机,以评估其表达能力.目前,针对SEFT时间特性进行分析的相关工作 较少.
因此,本文考虑采用合适的形式模型精确描述SEFT的语义并支持其时间特性分析.SEFT中顶层事件表示危害的发生,利用逻辑门连接构件表达危害发生的因果关系.构件内部行为采用有限状态机表达并同时描述功能与随机特性,通过端口与外部进行交互.因此,SEFT中的构件和逻辑门可以看作是通过接收特定的输入信号或产生输出信号与环境进行交互.SEFT构件内部的这种同时描述功能和随机时间的特征可以采用IMC进行描述,但由于IMC缺乏输入、输出动作的概念,难以有效地描述SEFT中构件之间的消息的发送与接收.所以,本文将IMC的交互动作精化为输入、输出动作,用于更精确地描述构件之间的交互行为.这样可以满足SEFT中同时描述功能和随机时间特性以及构件之间交互的需求,因此可以采用Interface-IMC严格描述SEFT的语义,以便支持后续的时间特性分析.
与已有的工作相比,本文根据SEFT的特点设计接口交互马尔可夫链对其语义进行描述,并设计相应的时间特性分析方法,为安全关键嵌入式实时系统的安全性评估提供支持.
7 总结与未来的工作本文针对状态事件故障树的时间特性分析提出了一种新的解决方法,主要工作包括:对交互马尔可夫链的交互动作语义进行了精化,建立接口交互马尔可夫链模型,并定义了并行组合用于描述构件的组合行为语义,以及弱互模拟操作用于约简状态空间;采用接口交互马尔可夫链对SEFT构件与逻辑门的语义进行精确描述,通过这些接口交互马尔可夫链的并行组合得到整个SEFT的语义模型,并在组合的过程中利用弱互模拟技术对状态空间进行约简;得到SEFT的严格语义模型之后,采用已有的时间特性分析工具IMCA对SEFT中顶层事件发生时间的最大和最小期望值进行计算;最后,以两个应用实例说明了本文方法的可行性.
下一步工作是构建更多复杂的系统实例,并且在接口交互马尔可夫链组合过程中,研究更为有效地减少状态空间的方法.在进行接口交互马尔可夫链并行组合的过程中发现,选择不同的组合顺序对所生成的状态空间的规模有较大的影响,因此,在未来的工作中将考虑如何得到最优的组合顺序.此外,还将进行基于接口交互马尔可夫链的SEFT概率特性分析以及系统的其他时间特性的分析.
附录:定理证明定理1. P1和P2是两个具有相同动作集的Interface-IMC,P3是一个可以与P1和P2进行并行组合的Interface- IMC,则:
(1) P1≈P2,则P1||P3≈P2||P3;
(2) P1≈P2,则P3||P1≈P3||P2.
证明:首先证明定理1中的情形(1).为了证明P1≈P2则P1||P3≈P2||P3,即证明P1≈P2的前提下,P1||P3与P2||P3满足定义3所定义的弱互模拟关系(即,满足定义3中弱互模拟定义的两个条件).
· 首先证明定理1中的情形(1)满足定义3中的第1个条件.
P1和P2是两个具有相同动作集的Interface-IMCs,令P是它们的并集且x≈Py,也就是说,存在一个P上的弱互模拟关系R,使得(x,y)ÎR.定义关系R¢如下:
由于R是P上的等价关系,显然,R¢是P||P3上的等价关系.
令(s||u,t||u)ÎR¢,(s,t)在R中.对于所有的aÎA,令
则存在s²||u²和s¢²||u¢²,使得sÞs²,uÞu², 
,s¢²Þs¢,u¢²Þu¢.根据并行组合的定义可知,
蕴含下列条件成立:
也即,
由于(s,t)ÎR,则存在一个t¢,(s¢,t¢)ÎR,使得:
从并行组合的定义可知,
从R¢的定义可知,(s¢||u¢,t¢||u¢)在R¢中.
从以上可以看出:定义3的第1个条件对于R¢也是成立的.
· 再证明定理1中的(1)满足定义3中的第2个条件.
从R¢的定义中可以推导出它具有以下等价类:
由于(s,s¢)ÎR当且仅当
对于等价类[s||u]R¢:[s||u]R¢={s¢||u|s¢Î[s]R},现令(s||u,t||u)ÎR¢,s||uÞs¢||u¢,s¢||u¢是稳态,C是R¢的等价类且C¹[s¢||u¢]R¢.根据并行组合的定义可知,这表示sÞs¢,uÞu¢且s¢和u¢是稳态.R¢的每个等价类可从R等价类和
中的一个状态导出.
令D是R的一个等价类,y为该状态,因此,C={s||y|sÎD}且u¢=y蕴含D¹[s¢]R.
注意到,如果u¢¹y,则s¢||u¢不在C中.C的后向闭包为
Cint={x¢||y¢|$x||yÎC.x¢||y¢Þx||y}={x¢||y¢|$xÎD.x¢ÞxÙy¢Þy}.
现在计算从s¢||u¢到Cint的累计转换率:
由(s,t)ÎR可知:sÞs¢且s¢是稳态蕴含存在一个t¢,使得tÞt¢,t¢是稳态,且(s¢,t¢)ÎR且对于所有的R的等价类除了[s¢]R之外有gM(s¢,Dint)=gM(t¢,Dint).显然,s¢和t¢在R的相同等价类中.现在可以得到以下结论:
因此,定义3中的第2个条件对于R¢也是成立的.对于任何状态
可知:如果(x,y)ÎR,则(x||z,y||z)ÎR¢.因为
R¢是弱互模拟关系,则x||z≈y||z得证.对于定理1中的情形(2),可以用类似的方法进行证明,因为并行组合具有完全的对称性.通过以上证明可以得出,本文定义的弱互模拟对于并行组合是同余的.
| [1] | Daskaya I, Huhn M, Milius S. Formal safety analysis in industrial practice. In: Proc. of the 16th Int’l Workshop on. Formal Methods for Industrial Critical Systems (FMICS 2011). LNCS 6959, Berlin: Springer-Verlag, 2011. 68-84 . |
| [2] | Bukowski JV. Defining mean time-to failure in a particular failure-state for multi-failure-state systems. IEEE Trans. on Reliability, 2001,50(2):221-228 . |
| [3] | Magott J, Skrobanek P. Timing analysis of safety properties using fault trees with time dependencies and timed state-charts. Reliability Engineering & System Safety, 2012,97(1):14-26 . |
| [4] | Kaiser B, Gramlich C, Forster M. State/Event fault trees—A safety analysis model for software-controlled systems. Reliability Engineering & System Safety, 2007,92(11):1521-1537 . |
| [5] | Elmqvist J, Nadjm-Tehrani S. Safety-Oriented design of component assemblies using safety interfaces. Electronic Notes in Theoretical Computer Science, 2007,182(29):57-72 . |
| [6] | Kaiser B. State/Event trees: A safety and reliability analysis technique for software controlled systems [Ph.D. Thesis]. Kaiserslautern: Universität Kaiserslautern, 2007. |
| [7] | Grunske L, Kaiser B, Papadopoulos Y. Model-Driven safety evaluation with state-event-based component failure annotations. In: Proc. of the 8th Int’l Symp. on Component-Based Software Engineering (CBSE 2005). LNCS 3489, Berlin: Springer-Verlag, 2005.33-48 . |
| [8] | Bryant RE. Graph-Based algorithms for Boolean function manipulation. IEEE Trans. on Computers, 1986,100(8):677-691 . |
| [9] | National Aeronautics and Space Administration. NASA Software Safety Guidebook, NASA-GB-8719.13, 2004. |
| [10] | Hersmans H. Interactive Markov Chains. Berlin: Springer-Verlag, 2002. |
| [11] | Zhang L, Neuhäußer M. Model checking interactive Markov chains. In: Proc. of the 16th Int’l Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2010). LNCS 6015, Berlin: Springer-Verlag, 2010. 53-68 . |
| [12] | De Alfaro L, Henzinger T. Interface automata. ACM SIGSOFT Software Engineering Notes, 2001,26(5):108-120 . |
| [13] | Crouzen P, Hermanns H, Zhang L. On the minimisation of acyclic models. In: Proc. of the Concurrency Theory 2008 (CONCUR 2008). LNCS 5201, Berlin: Springer-Verlag, 2008.295-309 . |
| [14] | Garavel H, Mateescu R, Lang F, Serwe W. CADP 2006: A toolbox for the construction and analysis of distributed processes. In: Proc. of the 19th Int’l Conf. on Computer Aided Verification (CAV 2007). LNCS 4590, Berlin: Springer-Verlag, 2007.158-163 . |
| [15] | Coppersmith D, Winograd S. Matrix multiplication via arithmetic progressions. In: Proc. of the 19th ACM Symp. on Theory of Computing. New York: Academic Press, 1990.251-280 . |
| [16] | Bouali A. Weak and branching bisimulation in FCTOOL. Technical Report, 1575, Valbonne Cedex: INRIA Sophia Antipolis, 1992. |
| [17] | Guck D, Han TT, Katoen JP, Neuhäußer MR. Quantitative timed analysis of interactive Markov chains. In: Proc. of the4th NASA Formal Methods Symp. (NFM 2012). LNCS 7226, Berlin: Springer-Verlag, 2012.8-23 . |
| [18] | Guck D. Interactive Markov chains analyzer. http://www-i2.informatik.rwth-aachen.de/imca/imc_analyzer.pdf |
| [19] | Stamatelatos M, Vesely W, Dugan J, Fragola J, Minarick J. Fault Tree Handbook with Aerospace Applications. Washington: NASA, 2002. |
| [20] | Maksimovic T. Data on reliability of sprinkler systems. 2011. http://dspace.vgtu.lt/bitstream/1/775/1/9_Maksimovic_S2.pdf |
| [21] | Ortmeier F, Schellhorn G. Formal fault tree analysis-practical experiences. Electronic Notes in Theoretical Computer Science, 2007, 185(13):139-151 . |
| [22] | Čepin M, Mavko B. A dynamic fault tree. Reliability Engineering & System Safety, 2002,75(1):83-91 . |
| [23] | Hansen KM, Ravn AP, Stavridou V. From safety analysis to software requirements. IEEE Trans. on Software Engineering, 1998, 24(7):573-584 . |
| [24] | Schellhorn G, Thums A, Reif W. Formal fault tree semantics. In: Proc. of the 6th Biennial World Conf. on Integrated Design and Process Technology (IDPT 2002). Pasadena: Society for Design and Process Science, 2002. 1-8. |
| [25] | Walker M, Papadopoulos Y. Qualitative temporal analysis: Towards a full implementation of the fault tree handbook. Control Engineering Practice, 2009,17(10):1115-1125 . |
| [26] | Palshikar GK. Temporal fault trees. Information and Software Technology, 2002,44(3):137-150 . |
| [27] | Reay KA, Andrews JD. A fault tree analysis strategy using binary decision diagrams. Reliability Engineering & System Safety, 2002,78(1):45-56 . |
| [28] | Bobbio A, Franceschinis G, Gaeta R, Portinale L. Exploiting Petri nets to support fault tree based dependability analysis. In: Proc. of the 8th Int’l Workshop on Petri Net and Performance Models (PNPM’99). IEEE Computer Society Press, 1999.146-155 . |
| [29] | Boudali H, Crouzen P, Stoelinga M. A rigorous, compositional, and extensible framework for dynamic fault tree analysis. IEEE Trans. on Dependable and Secure Computing, 2010,7(2):128-143 . |
| [30] | Magott J, Skrobanek P. Method of time Petri net analysis for analysis of fault trees with time dependencies. Computers and Digital Techniques, 2002,149(6):257-271 . |
| [31] | Merle G, Roussel JM, Lesage JJ, Bobbio A. Probabilistic algebraic analysis of fault trees with priority dynamic gates and repeated events. IEEE Trans. on Reliability, 2010,59(1):250-261 . |
| [32] | Höfig K, Domis D. Failure-Dependent execution time analysis. In: Proc. of the Joint ACM SIGSOFT Conf.—QoSA and ACM SIGSOFT Symp.—ISARCS on Quality of Software Architectures—QoSA and Architecting Critical Systems—ISARCS (QoSA- ISARCS 2011). New York: ACM Press, 2011. 115-122 . |
| [33] | Hu J, Yu XF, Zhang Y, Li XD, Zheng GL. Scenario-Based consistency verification of component-based Real-time system designs. Ruan Jian Xue Bao/Journal of Software, 2006,17(1):48-58 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/17/48.htm |
| [34] | Firley T, Huhn M, Diethers K, Gehrke T, Goltz V. Timed sequence diagrams and tool-based analysis—A case study. In: France R, Rumpe B, eds. Proc. of the 2nd Int’l Conf. on UML (UML’99). LNCS 1723, Berlin: Springer-Verlag, 1999.645-660 . |
| [35] | Zhang PC, Li B X, Li WR. Syntax and semantics of timed property sequence chart. Ruan Jian Xue Bao/Journal of Software, 2010, 21(11):2572-2767 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/3711.htm |
| [33] | 胡军,于笑丰,张岩,李宣东,郑国梁.基于场景构件式实时软件设计的一致性检验.软件学报,2006,17(1):48-58.http://www.jos.org.cn/1000-9825/17/48.htm |
| [35] | 张鹏程,李必信,李雯睿.时间属性序列图:语法和语义.软件学报,2010,21(11):2572-2767. http://www.jos.org.cn/1000-9825/3711.htm |