没有合适的资源?快使用搜索试试~ 我知道了~
理论计算机科学电子笔记185(2007)139-151www.elsevier.com/locate/entcs形式化故障树分析-实践经验弗兰克·奥特迈尔格哈德·谢尔霍恩LehrstuhlfuürSoftwaretechnikundProgrammiersprachenUniversitaet Augsburg奥格斯堡D-86135摘要安全性是许多现代系统的重要要求。为了确保复杂关键系统的安全,已经形式化了众所周知的安全分析方法。这尤其适用于自动化系统和运输系统。本文给出了应用最广泛的安全分析方法之一:故障树分析法(FTA)的形式化描述。 正式的FTA允许严格的原因关于故障树的完整性。这意味着有可能证明某个组件故障组合是否是不是系统故障的关键这是一个很大的进步,因为因果关系的非正式推理非常容易出错。我们报告我们的经验与现实世界的案例研究,从域的铁路。这里介绍的案例研究是-据我们所知-第一个完整的正式故障树分析的无限状态系统。到目前为止,只有有限状态系统已经分析了正式的FTA使用模型检查。保留字:故障树分析,可靠性,安全分析,形式化方法1引言近年来发生的许多重大事故表明,现代系统带来的风险正在上升(例如,最近中国化工厂的事故因此,安全性成为系统开发中越来越重要的问题与此同时,新系统变得越来越复杂。这使得安全分析变得更加重要和困难。因此,必须开发新的和更好的分析方法一种这样的技术是正式的FTA。FFTA是著名的FTA的正式变体其好处是,可以严格证明组件故障和系统故障之间的因果关系。这比非正式推理更不容易出错,并产生更好的结果。在本文中,我们提出了一个无限状态系统的第一个正式的故障树分析,我们面临的问题和我们学到的教训。我们使用[14]的形式故障树语义。使用KIV系统进行验证[2]。该案例研究也可以被视为如何在交互式验证环境中进行正式FTA的指南。从安全的角度来看,问题和解决方案1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi:10.1016/j.entcs.2007.05.034140F. 奥特迈尔湾Schellhorn/Electronic Notes in Theoretical Computer Science 185(2007)139在所提出的案例研究中发现的是一个大组的安全关键系统的典范。在第二节中,我们简要介绍了FTA,总结了形式语义,并回顾了Harel的状态图的语义第3节介绍了一个来自铁路领域的真实案例研究。经验教训见第4节。结论和展望是在节。五、2形式化故障树分析一种众所周知的安全分析技术是故障树分析(FTA,[16])。FTA是为技术系统开发的,用于分析它们是否允许危险(顶部事件)。顶部事件记录在故障树的根部。造成危害的事件在子节点中给出并递归分析,从而产生事件树。每个分析的事件(主事件)都通过故障树中的门与其原因(子事件)相连(见图1)。与门表示所有子事件都是触发主事件所必需的,对于或门,只有一个子事件是必需的。禁止门规定,除了子事件中所述的原因外,条件(椭圆形中注明)必须为真才能触发主事件。禁止门或多或少是一个与门,其中的条件不一定是故障。树的叶子(基本事件)是组件级的失效模式这些故障必须以某些组合(对应于树的AND/OR结构)发生,然后才能发生顶部事件,即系统故障。 故障树示例如图所示。8 .第八条。事件与门或门INHIBIT-gate基本事件图1.一、故障树符号导致危险的基本事件的组合称为割集。最小割集是一个割集,如果该割集上只有一个事件被预防,则该割集不会导致最高水平危险。一个典型的例子是,在冗余系统的系统故障,这是必要的,主要和次要单位故障(例如,电动和液压制动模块)。此信息有助于识别故障事件,排除这些故障事件可确保系统安全。例如,如果一个事件发生在不同的最小割集中,如果可以排除该事件,则顶级危险的概率将大大降低。最小割集可以从故障树计算相结合的主要事件与布尔运算符所指示的门。一个最小割集则由一个合取的析取范式的元素组成,F. 奥特迈尔湾Schellhorn/Electronic Notes in Theoretical Computer Science 185(2007)139141DDDC栅极ITL公式栅极ITL公式ψDQx(n→n1n2)ψC2);Qi )ϕ1ϕ2ϕ1ϕ2ψDQx(n→n1n2)ψCψAC2);Qi )<$(<$Qx<$1;Qi )<$(<$Qx )ϕ1ϕ2ψDχϕQx(λ→λλx)ψCχϕ<$(<$Qx();Qi )<$(<$Qx(x);Qi )图二. 故障树产生的公式。对于形式化的故障树分析,每个门由一个区间时序逻辑(ITL)公式表示。国际交易日志中的时间公式是根据一阶公式建立的,位置相关性和以下部分1:Qi(“in all initialint ervals(((“在某个子区间中“)和FTA的形式化表明,将OR门的语义简单地定义为析取是不充分的,因为它没有考虑到子事件(原因)通常发生在主事件(结果)之前,并且事件可能有持续时间。因此,有必要区分具有布尔语义的分解门(D-gates)和描述时间依赖性的因果门这导致了7种类型的门。图2中示出了门及其形式化。例如,示出了D门(左列)和C门(右列)的FTA公式。D-OR门和D-AND门(,)可以规范地定义:例如D-AND-gate()表示,无论何时发生排斥反应,第一和第二也必须发生。 一个C-OR-gates()声明,它不能是有可能分裂一个运行,这样,在上半场没有原因1和原因2发生,但结果1发生在下半场开始时。换句话说:如果结果发生了,其中一个原因必须在之前发生过(完全,如果它有持续时间,因此印章是必要的)。 原因和后果不能重叠。 异步和同步C-AND[1]ITL还定义了量化和许多其他这里不需要的导出算子。更多信息可参见[1]ϕ1ϕ2ϕ1ϕ2142F. 奥特迈尔湾Schellhorn/Electronic Notes in Theoretical Computer Science 185(2007)139CACDC门(,)是类似的,它们要求两个原因必须发生(在在此之前,后果。 D-INHIBIT-和C-INHIBIT-gate(,)与D-AND-gate和AC-gate相同。Hansen等人[8]在持续时间演算(DC,[17])中定义了因果门,但它们的定义不符合原因在结果之前完成的要求随后的出版物[7]仅限于分解门。Bruns和Andersen[4]也使用μ演算定义了故障树语义。它们还区分了因果门和分解门。只考虑没有持续时间的事件。对于这种特殊情况,我们的语义是等价的(详见[15])。对于图2中的语义,证明了以下定理:定理2.1(最小割集定理)如果故障树的所有条件都被验证,并且对于每个最小割集,至少有一个基本事件被阻止发生,那么顶层事件永远不会发生。这意味着在实践中,如果您验证故障树中每个门的相应公式,则可以确保您没有忘记故障树中的任何分支(即,没有“忽略”失效模式的组合换句话说,它是足够的,以防止每个最小割集的一个主要事件因此,完整的故障树是系统安全性的部分证明。它显示了组件故障的组合是系统故障的必要原因。完备性定理也给出了在定量安全分析中使用最小割集的正式证明,即使是在时间条件相关的情况下[13]。该定理证明使用结构归纳法的故障树的大小。证明的基本事实是因果关系的传递性。证明是用KIV系统([2])进行的,使用了连续区间时态逻辑的语法和语义的代数规范。2.1状态图在本文中,系统建模为状态图。状态图有几种不同的变体。最常见的是UML状态图和Statemate状态图。对于Statemate状态图,Harel和Damm [6]定义了形式语义。本文采用状态图作为系统模型。该语义已集成到Statemate[3],也得到了交互式定理证明器KIV [2]的支持。状态图可以被看作是传统状态转换系统的扩展。单个状态图包括一组(子)状态图、一组标记的转换和初始状态。图3显示了一个非常基本的状态图。状态图表My Chart有两个(子)状态图表:状态A和状态B。当且仅当事件ev被触发并且条件cond成立时,从状态A到状态B的转换发生。如果采取了转换,则将执行ActionAct。事件和条件之间的区别在于事件只有一个时间步是活动的(没有像UML状态图中那样的事件队列),而条件F. 奥特迈尔湾Schellhorn/Electronic Notes in Theoretical Computer Science 185(2007)139143我的图表ev[cond]/act状态_A状态_B图三. 基本状态图可以是任意的(非时间的)公式。因此,条件通常可以保持几个时间步长。 Act是一个类似C的程序,当 过渡就完成了。如果几个过渡是同时可能的,那么一个将被不确定地选择。Statemate状态图语义的更详细描述可以在工具的文档或[ 6 ]中找到为了形式证明的目的,事件和条件可以类比地处理。 从现在开始,我们将event[cond ] /act写成event[cond]/act。若无所作为有定义为我们简单地写event_cond。如果没有条件,也没有事件在守护transition(自发性转变),我们就用/act。未标记的跃迁是没有定义动作的自发跃迁。3为例作为一个应用正式FTA的例子,我们提出了一个基于无线电的铁路道口的分析。案例研究是使用交互式定理证明器KIV [2]完成的,证明工作量约为1.5人月。本案例研究是德国研究委员会(DFG)优先计划1064的参考案例研究。该计划旨在将现场测试的工程技术与软件工程领域的现代方法结合起来德国铁路组织Deutsche Bahn准备了一种新的技术来控制铁路道口:分散的、基于无线电的铁路道口控制。该技术针对中速路线,即最高速度为160 km/h的路线。在[10]中给出了概述。无线电通信中心局路线基本数据缺陷见图4。 无线电铁路道口该技术与传统的铁路-公路交叉口控制之间的主要区别在于,路线上的信号和传感器被火车和铁路交叉口中的无线电通信和软件计算所取代(见图4)。这不仅提供了更便宜、更灵活的解决方案,而且还将安全关键功能从硬件转移到软件。不是通过传感器检测到接近的列车,将此信息发送到关闭铁路道口的中央办公室,而是列车不断地计算144F. 奥特迈尔湾Schellhorn/Electronic Notes in Theoretical Computer Science 185(2007)139它必须发送信号以确保平交道口安全的位置这有效地节省了资金(轨道上不需要太多设备),并取消了中央控制系统(这是该地区所有列车的单点故障为了计算激活点,列车使用关于其位置、最大减速度和交叉口位置的数据。因此,火车必须知道铁路道口的位置,确保铁路道口安全所需的时间,以及其当前的速度和位置。前两项存储在数据存储中,最后两项由里程表测量。出于安全原因,安全裕度被添加到激活距离。这允许补偿里程表中的一些偏差。该系统的工作原理如下:列车不断计算自己的位置。当它接近一个十字路口时,它会向十字路口广播一个“安全”请求。当铁路道口收到“安全”命令时,它会打开交通灯,首先是“黄”灯,然后是“红”灯,最后关闭屏障。当它们被关闭时,铁路道口在一段时间内是列车路线上的在列车到达“最后制动点”(最后点,列车可能在道口前停车)之前不久,它请求铁路道口的状态。当道口安全时,它会发出“释放”信号,表明列车可以通过道口。否则,列车必须在交叉口前制动并停车。铁路道口定期进行自我诊断,并自动通知中央办公室有关缺陷和问题。中央火车站还负责维修,并为列车提供路线说明这些描述指出了铁路交叉口的位置该系统的安全目标是明确的:它绝不能发生,火车通过一个没有安全的道口一个设计良好的控制系统必须保证这一性质,至少只要没有组件故障发生。相应的危险是“火车通过道口,道口没有安全”。这是我们在本案例研究3.1形式化模型在下面的部分中,给出了该系统的状态图模型的简要描述。请注意,该模型不仅包括预期行为,还包括失效模式。这对于所有类型的正式安全分析都是必要的。关于如何从预期行为的功能模型导出此类模型的详细信息,请参见[12]和[11]。基于无线电的铁路道口模型分为三个平行的图表。一张图表模拟了交叉口,另一张模拟了通信,第三张模拟了火车。这三个图表解释如下。3.1.1穿越模型图5中的状态图显示了对列车发送的信号做出反应的交叉口的模型。最初,交叉口处于开放状态,这意味着F. 奥特迈尔湾Schellhorn/Electronic Notes in Theoretical Computer Science 185(2007)139145穿越打开不想要的_打开Pos>DS关闭计数≥T最大关闭关闭请求接收器/关闭计数= 0关闭关闭计数≥T最大关闭/Closed_Count = 0关闭SR CROSSING:状态请求接收错误(已关闭错误_已关闭)/发布Snd图五. 交叉图模型酒吧是开放的。当道口接收到来自列车的信号Close Request Rcv时,道口进入关闭状态。这将激活一个称为关闭计数的计时器,该计时器模拟在十字路口打开灯号和关闭酒吧所需的时间这需要时间(T最大关闭)。 在此时间到期后,过境点关闭(状态关闭)。另一个计时器Closed Count被启动,以确保条不会关闭太久。这是铁路组织的标准程序。如果列车通过危险点(位置> DS)或计时器达到T最大关闭,则道口重新打开。 如果检测到列车通过的传感器发生故障,道口也会打开其栅栏(意外打开)。交叉口对列车状态请求的响应如果它接收到状态请求(状态请求接收),则如果杆关闭(预期行为)或如果传感器对杆位置的检测存在错误(错误关闭),则将发送释放消息(释放Snd3.1.2火车模型列车的模型分为两部分:一部分用于对列车的物理进行建模,另一部分用于对控制器逻辑进行建模。从理论的角度来看,建议分别对列车的控制和物理进行建模。但在这个例子中,物理模型只包括一些静态反应(见图2)。6)。这些静态反应基本上表明,列车的位置根据速度更新,并且速度根据加速度更新。因此,为了更简单地表示,这两个部分已经合并。列车控制系统监控列车的位置,向道口发出关闭请求,并最终决定是否需要紧急停车。的146F. 奥特迈尔湾Schellhorn/Electronic Notes in Theoretical Computer Science 185(2007)139列车控制空闲闭合(位置、V、最大加速度、DS)/关闭请求WFC请求(位置、V、最大加速度、DS)/状态_请求_Snd制动Wfs计数>1次错误制动/A =最大加速度Wfs计数>1个错误制动器WFS发布_接收去火车SR_TRAIN:Tick/Pos:= Pos + V;如果V> A,则V:= V-A,否则如果V> 0,则V:= 0列车控制在列车上的软件中实现。正式模型如图6所示。从其初始状态空闲开始,图表进入状态Wfc根据实际速度、估计的接近和通信时间以及列车的最大减速度,持续计算发送该信号的时间点这在谓词Close(Pos,V,AccMAX,DS)中建模。一段时间后,列车到达另一个虚拟控制点,该虚拟控制点也是连续计算的,并在谓词请求(Pos,V,AccMAX,DS)中建模。 这是列车向道口发送状态请求(状态请求Snd)时的位置。然后,控件处于状态Wfs(“等待状态应答”)。如果列车在下一个Wfs计数时间单位内收到释放信号,控制器将进入Go状态,列车可以通过道口。否则,必须发出紧急停止。在这种情况下,制动器被激活(A=AccMAX),控制器进入制动状态。 制动器的故障也被建模。如果制动器失效,控制器仍将进入制动状态,但不会有真正的减速。 刹车和前进这两个状态是星盘的最终状态,所以它们见图6。 列车控制图模型3.1.3沟通模式这种沟通是由三种静态反应来模拟的,见图7。 这些静态反应代表了沟通的功能和功能障碍。功能通信中继所有传入消息,例如(SR COMM1)列车的关闭请求(关闭请求Snd)作为关闭请求Rcv转发到道口。如果通信失败(Failure Comm),则不会有消息到达接收器。另外两个静态反应代表状态F. 奥特迈尔湾Schellhorn/Electronic Notes in Theoretical Computer Science 185(2007)139147D列车在紧急停车点,紧急制动,未收到列车停在停车点,未收到门-7C列车在停车点,道口未关闭,释放信号发送门-4D门-5门-6C Cn)的o)的制动器故障制动时间过短列车在紧急停车点,A =0,紧急制动,未收到火车站A /0=,紧急制动,未收到门-9D火车站:DallasSpot,Dallas因传感器故障而打开列车未到达ds,道口开放,释放信号发送门-8C因传感器故障而打开杆传感器位置信号故障d)、道口未封闭D火车在交叉口,没有关闭,未收到通信SR COMM 1:关闭请求和故障通信/关闭请求接收SR COMM 2:状态请求和故障通信/状态请求接收SR COMM 3:释放请求和故障通信/释放接收请求(SR COMM2)和释放消息(SR COMM3)。见图7。 通信图模型3.2故障树分析这个模型现在用正式的FTA进行分析(见第2节)。有趣的危险是一种情况,火车经过十字路口,而酒吧没有关闭。我们称这种危险为该危险的故障树见图8。a)、b)、2号门e)、门-1Dc)、g)的3号门(一)h)的j)j)k)(l)(m)图8.第八条。 危险碰撞事故树列车在交叉口,交叉口未关闭列车还没有到达DS,道口未关闭,释放信号发送f)的148F. 奥特迈尔湾Schellhorn/Electronic Notes in Theoretical Computer Science 185(2007)139故障树的顶部事件(碰撞)可能有两个不同的原因。一种是列车通过道口,虽然没有发出放行信号,但道闸没有另一种是火车通过道口的情况F. 奥特迈尔湾Schellhorn/Electronic Notes in Theoretical Computer Science 185(2007)139149而杆没有关闭,但是已经发送了释放信号。第一个原因与列车的不当行为有关,第二个原因与交叉口的一 这两种不同的情况必须进一步分析。左侧节点-列车通过道口(道口未关闭时),虽然没有收到释放信号,但由于列车行为故障,因此不需要道口信息。这是一个D-抑制门。右侧节点,列车通过未封闭道口且已发出放行信号,可由两种不同情况引起。一种是列车接近未关闭的道口,并发出放行信号(道口未关闭时)。其原因可能是杆2的位置传感器中的故障。另一个可能的原因是,在释放信号发出后,但在列车通过道口之前,栏杆打开。原因可能是超时或请求打开栅栏的错误。另一个原因是列车通过开放/开放的交叉口,并且信号已经发送了一段时间。例如,前三个节点的形式化如表1所示。非正式节点形式化在危险地点训练,道口未封闭Posds≤Pos+V≤关闭在危险地点训练,道口未关闭,未收到放行信号Posds≤Pos+V≤关闭释放信号接收在危险地点训练,道口未关闭,释放信号发出Posds≤Pos+V≤关闭释放信号Snd表1故障树节点的然后,通过将这些节点的形式描述插入图1的D-OR-gate公式中,构建出最终的证明义务。其他故障树门被类似地处理。上述故障树已被证明是完整的。这意味着,对于每个门,都有相应的证明义务。结论是,对于这个例子来说,所有的最小割集都是单点失效的因此,系统中没有冗余。另一方面,故障树还表明,如果这些故障得到预防,则危害将不会发生。换句话说,如果没有什么失败,系统将按预期工作,甚至更短:2或如果与列车状态请求同时,一个(错误的)打开栅栏的请求到达交叉口。故障树的这个分支通常只能通过正式的FTA来找到。非正式FTA检测不到。150F. 奥特迈尔湾Schellhorn/Electronic Notes in Theoretical Computer Science 185(2007)139系统功能正确。4经验教训正如在摘要中已经提到的,这里介绍的案例研究是我们所知的第一个有限状态系统的正式安全分析。在本节中,我们将简要介绍我们在无限状态模型上证明FTA公式的经验为了证明故障树的正确性,我们使用KIV [2]作为交互式验证工具。KIV系统的一大优势是,它原生地支持状态图作为指定机制。第3节中所示的状态图模型可以直接用作KIV中的系统规范。证明义务源自上一节所示的故障树。它们也可以由KIV的故障树模块生成。KIV允许用符号执行和归纳来证明时间属性[1]。这意味着每个时态公式都被分成一个谓词逻辑部分和一些必须从下一步开始保持的属性在实践中,这会导致遍历状态图的所有可达状态,直到找到循环并可以应用归纳。状态爆炸可以通过泛化来避免。推广意味着不是证明一个公式,而是证明一个更一般的定理于是,起始公式是更一般的定理的特殊化这种类型的策略通常有助于交互式验证。案例研究总共需要大约一个半月的时间。我们在本案例研究中取得了以下经验:FFTA证明很容易,但很耗时。 几乎所有的验证步骤都可以自动完成 只有找到足够的概括和识别正确的归纳论点(即相应的状态)需要人的交互和技能。在大多数情况下,一般只能手动找到特别是对于大的证明,找到这个位置可能非常耗时(即已经证明了类似子目标的证明部分)。为了定位正确的点,似乎可以使用哈希函数。这将使状态图证明更容易和更快。泛化是一个很大的帮助,但不容易被发现(见上文)。很明显,越是普遍化,就越有可能成为继承国,反之亦然。例如,如果你分析一个确定性的状态图,那么在没有泛化的情况下,时间上的每一步都会导致一个新的状态。如果你概括这个状态图(也就是说,你抛弃了当前状态的所有信息),那么你将得到所有可能的状态,作为下一步的可能候选。在许多情况下,即使是这种“残酷”的概括也是有帮助的(例如,如果你必须证明火车是朝一个方向移动的)。虽然你可以在你的证明中得到多达200个案例的区别,但KIV系统可以通过其内置的谓词逻辑简化器关闭所有这些案例。这导致了两种方法来证明FTA属性:深度优先搜索和呼吸优先搜索。如果不清楚证明义务是否成立(即,如果故障树的节点已经F. 奥特迈尔湾Schellhorn/Electronic Notes in Theoretical Computer Science 185(2007)139151正确或不正确)。这对于验证公式和早期发现错误特别有用。广度优先搜索通常更快,但只能在最后发现指定错误。但是对于某些性质,甚至可以完全推广系统的状态,并在一步中完成证明形式化FTA节点是困难的。 即使对于简单的系统,也很难正确地形式化故障树的节点。这是因为对故障树的非正式理解(将原因分解为组件)不足以进行正式描述。如果所有的证明义务在一开始就以深度优先搜索的方式得到验证,根据我们的经验,这种额外的排序确实值得花时间,因为形式化故障树的节点非常容易出错。5结论我们首次用FTA验证了无限状态系统。我们的经验表明,具有交互式验证的正式FTA是一个有前途的,但不是一个容易的话题。许多问题都是由具体化错误引起的。这些问题可以用好的方法来解决与其它形式化的安全分析方法相比,形式化FTA是唯一一种具有人类可读和可理解的逻辑背景结构的方法,因此比按钮技术(如纯模型检测)更容易被工业界接受。引用[1] M.巴瑟带有符号执行的并发系统博士论文,奥格斯堡大学,奥格斯堡,德国,2005年。[2] M. Balser,W.赖夫湾Schellhorn,K.Stenzel和A.拇指使用KIV进行正式系统开发在T. Maibaum,编辑,软件工程的基本方法,LNCS第1783号,第363-366页。Springer-Verlag,2000.[3] T. Bi enmüoll er ,W. D amm , anddH. 是 的。STATEM ATE是一种虚拟现实技术。 在 大 肠 A.Emerson和A. P. Sistla,编辑,CAV斯普林格。[4] G. 布伦和S。 Ander s on. 在一个充满错误的现代化世界里, INJ。 G'orski,editorr,S afeC omp' 9 3:12th International Conference on Computer Safety,Reliability,and Security,pages 21 - 30. Springer-Verlag,1993.[5] A.卡乌湾Moszkowski和H. 泽丹 ITL 软件技术研究实验室,SERCentre,德蒙福特大学,网关,莱斯特LE1 9BH,英国,2002年。www.cms.dmu.ac.uk/.[6] W.达姆湾,澳-地乔斯科湾Hungar,和A.普努埃利STATEMATE设计的组合实时语义。在W.- P. deRoever,H. Langmaack和A. Pnueli编辑,COMPOSSpringer,1998年。[7] K.汉森,A. Ravn和V. Stavridou。从安全分析到软件需求。 IEEE软件工程学报,24(7):573[8] K. M.汉森,A. P. Ravn和V. Stavridou。从安全性分析到正式规范。ProCoS II文件[ID/DTH KMH 1/1],丹麦技术大学,1994年。[9] D. Harel 和 A. 娜 玛 德 statecharts 的 statemate 语 义 。 ACM Transactions on Software Engineering andMethodology,5(4):293[10] Klose 和 A. 拇 指 参 考 案 例 研 究 “V e r k e h r s l e itte chnik” 的 STATEMATE 参 考 模 型 。 TechnicalReport2002-01,Uiver s it?tAugsburg,2002.152F. 奥特迈尔湾Schellhorn/Electronic Notes in Theoretical Computer Science 185(2007)139[11]F. Ortmeier,A. Thums,G. Schellhorn和W. Reif. 结合形式化方法和安全分析- ForMoSA方法。在工程应用软件规范技术的集成。Springer LNCS 3147,2004年。[12] 弗兰克·奥特迈尔和沃尔夫冈·赖夫。运输控制系统的形式化安全分析 在SEFM 2005会议记录,2005年。[13] G. Schellhorn,A.Thums和W.赖夫形式化故障树语义。第六届集成设计过程技术世界会议论文集,Pasadena,CA,2002年。[14] A. 你好。 FommaleFehlerbaumanalyee. PhDthes is,UniversitüatAugsburg,Augsburg,Germamny,2004. (德文)[15] A. Thums,G.Schellhorn和W.赖夫比较故障树语义。In D.Haneberg,G.Schellhorn,andW. Reif,editors,FM-T00LS2002,Tech nicalReprt2002-11,第2 5 - 32页。 UniversitéatAugsburg,2002.[16] W. E. Vesely,F. F. Goldberg,N. H. Roberts和D. F.哈斯尔 故障树手册。 华盛顿特区,1981. NUREG-0492。[17] 周朝辰和M. R.汉森持续时间演算:逻辑基础。在Formal Aspects of Computing,第283-330页
下载后可阅读完整内容,剩余1页未读,立即下载
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://profile-avatar.csdnimg.cn/default.jpg!1)
cpongm
- 粉丝: 4
- 资源: 2万+
上传资源 快速赚钱
我的内容管理 收起
我的资源 快来上传第一个资源
我的收益
登录查看自己的收益我的积分 登录查看自己的积分
我的C币 登录后查看C币余额
我的收藏
我的下载
下载帮助
![](https://csdnimg.cn/release/wenkucmsfe/public/img/voice.245cc511.png)
会员权益专享
最新资源
- 京瓷TASKalfa系列维修手册:安全与操作指南
- 小波变换在视频压缩中的应用
- Microsoft OfficeXP详解:WordXP、ExcelXP和PowerPointXP
- 雀巢在线媒介投放策划:门户网站与广告效果分析
- 用友NC-V56供应链功能升级详解(84页)
- 计算机病毒与防御策略探索
- 企业网NAT技术实践:2022年部署互联网出口策略
- 软件测试面试必备:概念、原则与常见问题解析
- 2022年Windows IIS服务器内外网配置详解与Serv-U FTP服务器安装
- 中国联通:企业级ICT转型与创新实践
- C#图形图像编程深入解析:GDI+与多媒体应用
- Xilinx AXI Interconnect v2.1用户指南
- DIY编程电缆全攻略:接口类型与自制指南
- 电脑维护与硬盘数据恢复指南
- 计算机网络技术专业剖析:人才培养与改革
- 量化多因子指数增强策略:微观视角的实证分析
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
![](https://img-home.csdnimg.cn/images/20220527035711.png)
![](https://img-home.csdnimg.cn/images/20220527035711.png)
![](https://img-home.csdnimg.cn/images/20220527035111.png)
安全验证
文档复制为VIP权益,开通VIP直接复制
![](https://csdnimg.cn/release/wenkucmsfe/public/img/green-success.6a4acb44.png)