理论计算机科学电子札记99（2004）111-126www.elsevier.com/locate/entcs应用广义非演绎成分（GNDC）方法在可靠性S.格内西湾Lenzini1Istituto di Scienze e Technologie Informatiche -C.N.R. Via G. Moruzzi 1，I-56100比萨，意大利F. 马蒂内利2Istituto di Informatica e Telematica - C.N.R.Via G. Moruzzi 1，I-56100比萨，意大利摘要本文提出了一个框架，其中可靠的系统可以统一建模和依赖的属性分析内的广义非演绎组合（GNDC），一个计划，已被有益地用于定义和分析的安全属性。 准确地说，我们的框架需要一个系统建模使用正式的演算，在这里的CCS进程代数，在失败的行为的系统和相关的故障恢复程序也明确描述。 一个能够在系统中注入任何故障的环境被定义为一个独立的组件。系统和环境之间的并行组合代表了我们的分析场景，其中一些容错属性（例如，故障停止、安全和静默）作为GNDC属性的实例进行研究。通过使用GNDC的不同实例，我们能够讨论有效分析方法的可用性，以及应用组合技术的可能性。保留字：可靠性、容错性、安全性、非干扰性、形式验证。我说：{stefania.gnesi，gabriele.lenzin i}@i sti. C NR. It2电子邮件：fabio. iit.cnr.it1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.02.005112S. Gnesi等/ Electronic Notes in Theoretical Computer Science 99（2004）111-1261介绍本文利用可靠性分析机制和安全性机制之间的关系，在一个正式的框架。更确切地说，它展示了容错分析机制如何从安全分析的最新结果中受益。关于安全分析策略和可靠性分析机制之间的关系的第一个想法可以在[14，15，10，21，22，25]中找到。例如，在一篇开创性的论文[25]中，韦伯发现了容错规范和非干扰定义之间的类比[8]。他还认为，容错的形式化验证面临着与安全验证类似的问题和相同解决方案的好处。安全分析中的非干扰方法之间的类比可以在[22]中找到。在利用容错方法进行安全分析中的其他研究可以在例如[7]中找到，其中示出了容错和完整性分析都可以基于非干扰概念。在[12]中，无干扰分析已被证明类似于开放系统的验证，即，当需要验证系统w.r.t.任何可能的执行环境（也称为鲁棒性）。值得注意的是，Meadows在[14]中讨论了在安全中应用可靠性方法的想法，她还认为安全分析可以通过引入可靠性正式验证的典型技术另一方面，Meadows和McLean在[15]中也声称，在安全分析中使用新兴结果可以丰富故障预防和删除策略的分类。无论如何，正如以前的工作似乎表明，很长一段时间以来，安全性已经出现了一个受限制的范例，这是一种依赖性中可用的各种方法。文献中的大多数讨论更多地基于从可靠性背景和经验开始寻找安全性的直觉，而不是相反。在过去的十年中，安全已经被深入研究，安全理论对可靠性的贡献比过去更多。例如，我们认为广泛用于安全分析的不干涉概念（例如，参见[4，3，13，20，24]），可以通过考虑到目前为止在安全领域中开发的非干扰分析技术，在可靠性框架沿着这个方向，本文打算探讨应用广义不可演绎组合（简称GNDC）的可靠系统的分析，特别是容错的。GNDC在[6]中首次引入，作为一个框架，可以统一表达和验证一系列安全属性。到目前为止，它从未被应用于可靠性无论如何，GNDC在非-S. Gnesi等/ Electronic Notes in Theoretical Computer Science 99（2004）111-126113一一干扰分析，其直觉已被声称与某些容错分析策略共享共同的思想（例如，见[7，23]）。一般来说，GNDC属性具有以下形式：P符合GNDCα（P）i <$$>X∈Env：（P<$X）a α（P）（1）非正式地说，它意味着系统P享有GNDCα（P）当且仅当P显示，w.r.t.一个特定的行为关系a，与α（P）的行为相同。即使P由并行运算符与任何环境X组合，这也必须成立。性质（1）在a中是参数的，a是代表“观察”概念的过程之间的关系在本文中，我们将展示如何利用这样的GNDC制定表达安全特性特有的可靠性分析：故障停止，故障安全，故障沉默。它构成了对可靠属性的正式分类的一步，类似于它在安全中发生的情况[5]。 此外，我们将展示GNDC的一些理论结果（例如，组合推理）最初用于安全分析（例如， 见[5]），可以在可靠性分析中重新陈述和重复使用。本文的结构如下。第2节描述了如何在CCS中按照统一的建模风格对容错系统进行建模第3节介绍并解释了GNDC的容错特性。第4节直观地介绍了GNDC方案中如何表达第五节讨论了可靠性分析问题它显示了如何使用基于迹的行为等价的容错特性的GNDC表征，将在分析中享有一些吸引人的特性，例如分析过程的有效性和组合性。第六节是论文的总结。2容错系统为了对系统建模，我们将使用进程代数。这里我们参考CCS [16]，但我们的框架是完全通用的，也可以很容易地对其他进程代数进行重述（例如， ，CSP [9]或π-演算[19]）。2.1CCS背景CCS语言假设一组通信动作来表示发射的信号或接收的信号。特殊符号τ用于模拟任何，无法被外界观察到的内部行为假设通信标签的集合L，Act = L L是可见动作的集合（即，、行动和114S. Gnesi等/ Electronic Notes in Theoretical Computer Science 99（2004）111-126defco-actions），并且Actτ=Actτ{τ}表示可能的通信动作的全集。我们让a，b在Actτ上变化。总之，定义所有CCS过程的语言语法如下：P，Q：：= 0|a.P|P + Q|P Q|P\L|P [f]|非正式的0是不执行任何操作的进程; a.P是操作前缀运算符; P+Q可以非确定地在过程P的行为或过程Q的行为;P\L是动作限制算子，这意味着标签a∈ L可以只能在通信中执行 P [f]是重标记运算符，将每个标签a重命名为f（a）。最后，我们假设每个过程标识符A都有一个形式为A=P的定义方程。CCS的语义是在有标签的变迁系统上操作给出的（参见[16]），其变迁关系→定义通常在一个步骤中推导出的概念：P→a PJ这意味着过程P通过执行动作a∈Actτ，在过程sPJ，而我们写为P→a 为了强调Pcnperformact iona，在某个过程中进化我们将写为→传递闭包和递归闭包关于a∈Actτ →a. 在下面的例子中，我们将使Der（P）={PJ|P→PJ}，排序（P）是由P使用的标签的集合，并且EF={X：Sort（X）<$F <${τ}}，其中F是一系列的行动2.2容错系统利用进程代数可以为容错系统的规范化提供一个统一的框架例如，在[1，2]中，CCS的一个变体被用于对系统、其故障行为、其恢复策略和其故障假设（即，故障发生的假设）;通过模型检查在系统的有限状态模型上验证表示为逻辑公式的容错特性。这里我们将遵循类似的建模方法，但与[1，2]不同的是，我们不需要在系统的正式模型中明确描述任何特定的故障假设。事实上，我们主要感兴趣的是评估系统在一般和未指定的故障环境中的行为。换句话说，我们把容错分析看作是对一个开放系统的分析[13]，该系统在一个可能引起系统中任何故障的环境中运行。在下文中，当讨论容错系统的形式模型时，我们将参考以下定义：一个系统模型是一个CCS过程P，通过动作的执行来它一般是一个并行的子流程组成∗S. Gnesi等/ Electronic Notes in Theoretical Computer Science 99（2004）111-126115FFFF FFF对方. Q一个失败的系统模型是一个CCS过程PF，通过扩展过程P的可能性，执行特定的外部动作从一组F可能的故障动作。在每个故障动作之后，例如通过描述由故障发生引起的行为，也在PF中指定相对故障模式Q一个容错（候选）系统模型是CCS进程P#，它是在PF上增加一些实现错误恢复策略的进程，采用某种容错设计策略（例如，组件的副本、三重模块冗余、表决等）。一般来说，容错技术在建模中的应用会导致过程P#，该过程可能是可解的。在CCS符号中表示为：P#=（P（1）··P（n）Q）\AF F F其中（a）P（1）. P（n）是P的n个拷贝（b）Q是a表示附加组件或错误检测模块的过程，（c）A={a1，· · ·，an}，ai∈/ F，a是P（i）与Q之间的同步作用的L个下界.Q故障的发生是由故障注入器过程FF引起的，其导致故障发生。它通过f∈F作用与P#精确地相互作用Q前面的定义收敛到下面的容错分析场景，其中系统模型和故障注入器组合在一起：场景=（PF#FF）\F（2）值得注意的是，在（2）中，故障动作是隐藏的，即，限制。这意味着PF和FF必须在故障事件上同步。因此故障被认为是内部的（即，不可观察的）故障系统的动作。这意味着我们的分析是在抽象层次上的，在这个层次上，真正可观察到的只是一个系统，但不是单一的故障发生。因此，在我们的框架中，粗略地说，容错意味着故障不能干扰系统的正常可观察行为注意，与其他方法（例如，[1]），我们假设故障行为在系统PF#中描述，而不是也在故障注入器FF中描述。这是将容错分析编码为非干扰分析并最终编码为GNDC分析的技术技巧。示例2.1作为一个经典示例，我们将给出一个简单容错系统的CCS模型。基本组件是一个模块电池，116S. Gnesi等/ Electronic Notes in Theoretical Computer Science 99（2004）111-126defdef我我defFdef当它接收到请求时返回一个能量时隙。为了简洁起见，我们将使用值传递样式CCS来编写示例，这是CCS的捷径[16]。动作get和ret用于传递模块的输入和输出：电池=获取。ret（1）. 电池在对相应的故障模块建模时，我们假设电池在接收到请求之后可能崩溃并且非确定性地产生有效能量槽（1）或无效能量槽（0）：电池f=获取。（ret（1）. 电池fΣ+小麦赤x∈{0，1}（ret（x）. 电池f））根据我们的建模框架，故障被假定为由环境触发的特殊故障动作f引起容错电池可以例如通过使用具有两个电池、具有分离器分离器和控制器控制器的附加模块的冗余来设计。我们要求分离器将能量请求分别传递到两个冗余实例中的每一个，分别是电池（1）和电池（2），而我们要求收集器通过吸收最终额外的槽来避免能量的过载产生。形式上，电池的两个实例及其故障对于i∈ {1， 2}，版本为：Battery（i）d=efBattery[get/get，ret/ret]Battery（i）d=efBattery[get/get，ret/ret]菲菲分离器和控制器例如是以下过程：Splitter= get。得到1。得到2。ack. 分离器控制器= ret1（x1）。ret2（x2）. ifx1then ret（x1）. ack.Controllerelse ret（x2）. ack. 控制器注意同步分离器和控制器所需的动作ack。例如，可以通过在冗余解决方案中插入单个故障模块来获得电池Batteryf#的所得容错模型（也参见图1）：Batery#d=ef（Spl i t ertBatery 1）电池2控制器）\{get，get ret1，ret2，ack}f12S. Gnesi等/ Electronic Notes in Theoretical Computer Science 99（2004）111-126117一F得到FFig. 1. 电池f#的流程图。内部行动在括号内。容错分析的结果场景如下：场景=（电池f#电池Ff）\{f}3GNDC中的容错特性本节报告了GNDC的基本思想，并解释了如何在GNDC方案中表达容错从第1节我们已经知道GNDC属性具有以下一般形式：P符合GNDCα（P）i <$$>X∈Env：（P<$X）a α（P）该方案足够通用，可以实现广泛的安全属性定义。事实上，例如，更具体的安全属性，如基于双模拟的非演绎组合（BNDC）和基于迹等价的非演绎组合[3]，可以归入GNDC属性。在容错中实例化GNDC所需的第一步是指定P和Env在此上下文中是什么。前者是遵循第2节中介绍的统一建模框架获得的流程P#。后者是所有故障注入器的环境（例如，我们的故障假设模型），即行动字母表为F的CCS过程的集合。正式Env = E F={X|Sort（X）<$F<${τ}}。然后，一般的GNDC方案，我们提出的容错，然后是以下内容：定义3.1[GNDC中的容错特性]Psatis fiesGNDCα（P）iFF∈EF：（P#FF）\ Faα（P#）（3）a让我们观察到，第2节（2）中系统模型和环境之间的明确分离将允许我们不指定FF（确认）（get1）电池（1）（ret1）分离器控制器ret（get）2电池（2）F（ret2）118S. Gnesi等/ Electronic Notes in Theoretical Computer Science 99（2004）111-126FFFFdefFFFdef并使其在EF范围内变化。此外，GNDC在容错中的实例化要求α（PF）适合于表达容错的一些基本性质（例如， 故障安全、故障静默、故障停止）。最后，我们有兴趣了解什么家庭的等价性A可以适用于分析这样的属性。 这将是下面几节的论点，当不需要显式引用第2节的规范框架时，我们将写P而不是P #。4GNDC的容错特性在本节中，我们将直观地介绍如何在GNDC方案中表达一些有趣的容错属性。一般来说，属性通过P的修改版本α（P）来建模，表示预期行为P。例如，如果我们假设一个故障停止属性，α（P）必须表示P的一个修改后的行为，其中任何故障的发生都必然导致系统停止。我们假设如果P是一个有限态过程，那么α（P）也一定是有限态的。失败停止一个系统P #的模型在发生故障的情况下，最终在执行了一些内部操作后，它将切换到停止状态，预计将失败停止。 直觉α（P #）是其扩展表达（即，通过应用展开定律[16]展开过程项而获得的树）是由PF中的一个通过将每个故障动作（和相关子树）替换为过程之后的无声动作而获得的0. 例如，参考我们的例子，我们有：αstop（Batteryf）= get。（ret（1）. 电池f + τ。0个）故障安全系统P #的模型预期是故障安全的，如果在故障的情况下它切换到安全状态。在这种情况下，α（P#）是这样的过程，其扩展表达式是通过将每个故障动作（和相关子树）替换为静默动作，然后再替换一些故障动作，从PF中的一个获得的。“安全行为”（例如，关闭）。 例如，我们有：αsafe（Battery f）= get。（ret（1）. 电池组f + τ.Psafe），其中Psafe对特定的“安全”行为进行建模。如果忽略故障，则系统P #的模型预期为故障静默。在这种情况下，α（P#）的扩展表达式是在将每个故障动作（和相关子树）替换为静默动作之后从PF之一获得的表达式，静默动作之后是对非故障动作建模的子树。失败的行为换句话说，每一次故障发生和任何连续S. Gnesi等/ Electronic Notes in Theoretical Computer Science 99（2004）111-126119FdefFF失败的行为被无声的行动所取代。例如，我们有：αsilent（P）= get. （ret（1）. 电池f + τ。电池f）容错一个系统P#的模型被期望是容错的，如果它的行为在观察上等于模块的行为，一点也不失败 在这种情况下，则αft（P#）=P#\ F，即故障F F容错系统永远不会执行任何错误操作。5GNDC中的容错分析策略本节提供有关GNDC方案中的容错分析的更深入的细节。5.1基于弱互模拟的GNDC容错算法我们可以使用弱互模拟来验证系统模型P#是容错的，w.r.t.容错性能之前描述的条款α（P#）。 事实上，如果外部观察者看不到τ作用，认为两个过程是等价的一种自然方式是从它们的行为中抽象出这些作用让考虑到CCS项之间的以下关系：如果P−→τPJ，∗α和PJ如果τ α τPJ。 我们从《易经》中可以看出，=PP−→ −→弱互模拟（即，观察）之间的过程需要两个双相似过程能够逐步相互模拟：定义5.1E× E上的对称关系B是弱互模拟，如果对每个（P，Q）∈B和每个a∈Actτ：如果P−→aPJ，n≠QJ：Q=aQJ和（PJ，QJ）∈B两个过程P和Q是双相似的（记作PbisimQ），如果一个互模拟B存在使得（P，Q）∈B。弱互模拟手段对于检测我们迄今为止定义的大多数安全特性是有用的，即故障安全、故障静默、故障停止和容错（分别由，αstop、αsilent、αsafe和αft）。 一些活性特性（例如， 死锁自由）也可能被捕获。此外，让我们观察到GNDC的实例，其中a是非对称的，并且其中α（P）是α ft（P #）= P # \F（即，确切地说是F F是在我们的容错框架中重新陈述的BNDC。 事实上αft（P#）##P满足GNDC要求Fbisimi FF∈EF：（PFFF）\FF（4）120S. Gnesi等/ Electronic Notes in Theoretical Computer Science 99（2004）111-126比塞姆我们提醒大家定义5.2[[3]]P是BNDCi <$$>X∈EF：（P<$FX）<$bisimP\F命题5.3（[6]）P是BNDC当且仅当P是GNDC P\F。作为最后的观察，让我们讨论BNDC不是合成w.r.t.。平行合成（见[12]），即从P，PJ∈BNDC不能推出P<$PJ∈BNDC。这在分析中可能是不期望的性质。无论如何，有基于互模拟的等价物是复合的，位置（例如，参见[3]中的SBSNNI），从而它们可以用来证明容错的充分条件，从这个观点来看，[4]中给出的容错公式是有吸引SBSNNI的使用不是在分析中获得组合性的唯一方法。如我们在5.2.2节中所解释的，可以使用不同的观测等价而不是（3）中的弱互模拟关系来获得它的替代策略。5.2用于容错弱互模拟对于检测到目前为止定义的大多数属性都是有用无论如何，让我们观察一下，在实际情况下，我们期望许多系统在满足较弱条件时是容错的。一般来说，只要系统对这些故障的行为响应“足够好”，就可以推断出故障的存在。例如，（4）中给出的容错定义似乎太强，阻止观察者推断出任何故障已经发生。在死锁检测之外，对于本文中定义的所有安全属性，区分分支结构的能力不是必需的或必要的，甚至是危险的：事实上，安全属性，非正式地可以读作[11]像这使得我们求助于弱形式的观测等价，例如迹等价和模拟，在GNDC理论中，它们也将对组合性和避免故障注入器在故障环境中的普遍量化产生积极影响在下文中我们我将写PFQ作为（PQ）\F的快捷方式，我们将引用一个泛型function. 显然，结果对我们的所有α（）5.2.1最一般（Favorite）环境避免表达式（3）中的泛量化器的可能性基于以下关于预同余的理论。 我们会说a是一个预同余w.r.t. <$F如果对每个P，PJ，X，∈EF如果PaPJ那么P<$FX a PJ <$FX. 的S. Gnesi等/ Electronic Notes in Theoretical Computer Science 99（2004）111-126121一da=P以下结果对于预同余成立：命题5.4（[6]）设a是a的预同余。1996年如果存在一个过程Top ∈ EF，使得对于每个过程X ∈ E F，我们有X a Top，那么：P∈GNDCα（P）i <$（P<$FTop）a α（P）特别地，如果上述命题的假设成立，则足以检验当P与最一般的环境Top组合时α（P）是满足的。在我们的容错分析上下文中，它只允许进行一次检查，以证明容错特性在每个故障场景中都成立。对于由a诱导的同余，我们也有以下推论：推论5.5（[6]）设a是关于t的预同余。设da定义为aa−1。如果存在两个过程Bot，Top∈ E F，使得对于每个过程X∈ E F，我们有Bot aXaTop，则P∈GNDCαi（PFBot）da（PFTop）daα（P）我们表明，每当我们感兴趣的性质的基础上的概念，跟踪等价，命题5.4和推论5.5举行。让一a = a1. an∈Act是一系列动作。 我们写PJ，如果和如果存在P，...，P∈E使得Pa1a2=anP. 设是1n= 1P1= 1.nT（P）={a∈Act<$：<$PJ，Pa j与过程相关联的迹集=P}P.我们拥有：定义5.6设P和Q是两个过程。此外，Q可以执行P的所有迹（写为P≤迹Q）当且仅当T（P）<$T（Q）。P和Q是迹等价的（记为P迹Q），当且仅当T（P）=T（Q）。很容易证明≤trace是关于CCS算子的预同余。命题5.7 ≤迹是一个预同余。 F证据 通过对转换规则结构的推理。Q此外，我们可以证明最一般的（失败的）环境的存在，并提供其描述。让我们考虑以下过程：上F=下F。顶部F+ f。（5）汽车旅馆f∈F很容易证明：122S. Gnesi等/ Electronic Notes in Theoretical Computer Science 99（2004）111-126def命题5.8如果X ∈ E F，则X ≤traceTopF。证据 通过对X射线产生的迹线长度的归纳，Q从而证明了存在一个关于≤迹的最一般的环境.当考虑以下模拟关系时，可以获得类似的结论：定义5.9 [[18]]设S是E × E上的二元关系。则S被称为a模拟如果对于每个（P，Q）∈ S和对于每个a∈Actτ，如果P一−→P J然后有xistsQJsuchthatQ=Qj和（PJ，QJ）∈S.如果存在一个模拟S使得（P，Q）∈ S，则记Q ≤ sim P. 很容易证明≤sim是关于CCS算子的预同余，在（5）中承认相同的最一般环境。命题5.10下列结果成立(i) ≤ sim是w.r.t.的预同余。 F(ii) 如果X ∈ E F，则X ≤ simTopF。证据（1）通过转换规则结构的推理，（2）通过对X产生的迹的长度的归纳。Q作为结论，当≤trace和≤sim被用作进程关系时，为了检查P满足GNDC属性，只能针对“最一般的（错误的）环境”执行不干涉的工具[12]。5.2.2容错的组成分析本节说明，当≤trace和≤sim在我们的分析方案中用作过程等价时，系统享有GNDC可以申请。组合性是验证中利用局部容错结果推断全局容错的理想让我们用一个简单的例子来说明它，这个例子是用以下过程扩展example2.1Torch= get. ret（x）. [如果x = 1，则闪烁，否则不闪烁]。0Sd=ef（Torchbatteryf#）\{get，ret}表示使用示例2.1的容错激励器的电火花炬的行为。即使在故障的情况下，增能器也被期望提供一个单位的能量。当接收到一个单位的能量时，火炬会发出闪光，否则不会发出闪光。什么S. Gnesi等/ Electronic Notes in Theoretical Computer Science 99（2004）111-126123≤simdef≤sim≤sim观察通过组成手电筒和激发器而获得的系统S的观察者期望仅看到闪光动作。（回想一下，系统Batteryf#只提供ret（1）。这种安全特性可以形式化为：S∈GNDCα（S）I I II∈Ef：SfFf≤sim α（S）=闪光。0其中使用了≤sim关系。在这种情况下，预期的行为（通过α（S）给出）是提供一个单位的能量（因此一次闪光观察）。很容易使我们相信，系统的给定规范享有我们的安全属性。现在让我们考虑一个系统Sn，它是由系统S的n个实例组成的（并行），并且在Sn上有一个类似的安全性，它反映了“最多只能观察到n个哈希”的问题在我们的方案中，这等价于证明：Sn∈GNDCα（S）nI I II∈Ef：Sn<$fFf≤sim α（S）nd=efα（S）.. . α（S）“我的天，n组合性将使前面的陈述为真，对于任何固定的n，不需要任何额外的检查。下面我们证明当使用≤ trace或≤ sim时确实是这种情况。以下结果成立：命题5.11设P1对于i = 1，2. 然后和p2是两个过程，使得Pα（Pi）≤痕量• P1• P1P2P2α（P1）<$α（P2）≤痕量∈GNDCα（P1）<$α（P2）证据利用最一般的环境Top的存在性，以及≤trace（或≤sim）是预同余的事实。Q必须对组合性的适用性进行最后的讨论利用这一节的结果，可以从局部容错性推导出全局容错性。在这里，我们用局部容错来表示子系统的形式规范所享有的属性，这些子系统需要自己容错。对于全局容错，我们指的是系统的具体化所享有的属性，该属性是通过这样的子系统的组合而获得的，而没有任何其他全局模块的伴随显然，我们并不期望组合性在这种情况下成立。这一讨论值得更好地发展，但由于远离本文的范围，我们将其留给未来的工作。∈GNDC∈GNDC124S. Gnesi等/ Electronic Notes in Theoretical Computer Science 99（2004）111-1266结论在本文中，我们展示了如何在GNDC框架内形式化容错，即， 在进程代数上下文中表示安全属性的一般方案。一旦被表征为GNDC属性，容错可以受益于各种理论结果和分析技术。这些结果和策略是证券分析研究背景所特有的具体而言，当使用迹线或模拟关系来表征容错特性时，GNDC理论确保存在有效的分析程序。具体而言，它既有利于静态表征（摆脱了对所有可能故障场景的普遍量化），又有利于组合性证明。我们统一表征的另一个优点是可以比较可靠性属性，就像在GNDC框架中对安全性属性所做的那样。这可能是迈向可靠性和安全属性的正式和统一分类的初步步骤。无论如何，本文的总体贡献旨在更广泛。事实上，通过这项工作，我们打算维持的趋势，手表在安全作为一个研究领域，其应用程序的可靠性分析仍在出现。如果考虑到最近出现在文献中的大量关于安全的结果，这是最有理由的。我们离开作为一个未来的工作，以扩大我们的研究在其他可靠性属性的表征致谢。所有的作者感谢匿名推荐人的有用建议，这些建议有助于改善工作的整体Gnesi和Lenzini得到了MIUR-CNR项目SP 4和MIUR项目MEFISTO的部分支持。Martinelli得到MIUR的支持项目引用[1] C. Bernardeschi，A. Fantechi和S.格内西容错系统的模型检验。软件测试、验证和可靠性，12：1[2] C. Bernardeschi，A. Fantechi和L.西蒙奇尼正式验证容错系统设计。The Computer Journal，3（43）：191[3] R. Focardi和R. Gorrieri。安全属性的分类。Journal of Computer Security，3（1）：5[4] R.福卡尔迪河Gorrieri和F.马蒂内利用于密码协议分析的无干扰。 在proc 第27届自动机、语言和编程学术讨论会，第354-372页，2000年。S. Gnesi等/ Electronic Notes in Theoretical Computer Science 99（2004）111-126125[5] R.福卡尔迪河Gorrieri和F.马蒂内利安全属性的分类-第二部分：网络安全。In R. Gorrieri和R.Focardi，编辑，安全分析和设计基础II，LNCS第2946卷，第139-185页。Springer-Verlag，2004.FOSAD 2001/2002年专题讲座。[6] R. Focardi和F.马蒂内利定义安全属性的统一方法。在Proc. of Congress on Formal Methods（FMSpringer-Verlag，1999.[7] S. N.福利外部一致性和安全协议的验证。在Proc. of the 6th International Workshop onSecurity of Protocols，Volume 1550 ofLecture Notes in Computer Science，pages 28-33中。Springer-Verlag，1998.[8] J. Goguen和J. Meseguer。安全策略和安全模型。IEEESymposium in Security and Privacy.IEEE Computer Society Press，1978.[9] C. A. R. 霍尔通信顺序进程。Prentice-Hall，Englewood Cli Jersey，NJ，1985年。[10] E.约翰松湖Stromberg和S. 林德斯科格 论安全性与可靠性损伤的函数关系。载于加拿大安大略省新安全模式讲习班论文集，1999年。[11] L.兰波特时间逻辑有什么好处。In R. E. Manson，编辑，IFIP信息处理大会论文集，第657-668页，阿姆斯特丹，1983年。北荷兰。[12] F.马蒂内利部分模型检查和定理证明以确保安全性。 第11届IEEE计算机安全基金会研讨会论文集，第44-52页。IEEE，计算机学会，1998年。[13] F.马蒂内利开放系统安全协议分析。Theoretical Computer Science，1（290）：1057[14] C.梅多斯将可靠性范例应用于计算机安全。新安全范例研讨会的论文集，第75-81页，1996年[15] C.梅多斯和J·麦克莱恩。安全性和可靠性：过去和现在。计算机安全，可靠性和保证研讨会：从需求到解决方案，第166Los Alamitos，CA，USA：IEEE Comput.Soc，1999，1998.[16] R.米尔纳通信和并发。国际计算机科学系列。普伦蒂斯·霍尔1989年[17] R.米尔纳并发进程的操作和代数语义。在J. van Leewen，编辑，Handbook of TheoreticalComputer Science，卷B：Formal Models and Semantics，第19章，第1201-1242页。麻省理工学院出版社，纽约，纽约，1990年[18] R.米尔纳通信和移动系统：π演算。剑桥大学出版社，1999年。[19] R. Milner，J. Parrow，and D.沃克移动过程的演算。信息与计算，100（1）：1[20] A. W.罗斯科，J.P.C. Wookcock和L.沃尔夫不干涉决定论。Journal of Computer Security，1（4）：27[21] J·拉什比关键系统属性：调查和分类。可靠性工程与系统安全，43（2）：189[22] J·拉什比安全和安全的分区：需求，机制和保证。技术报告CR-1999-209347，NASA兰利研究中心，1999年6月[23] J·拉什比安保、安全和分隔。2003年11月4日至6日，日本东京，软件安全国际研讨会（ISSS。出现在计算机科学讲义中。126S. Gnesi等/ Electronic Notes in Theoretical Computer Science 99（2004）111-126[24] A. Simpson，J. Woodcock，and J. Davis.安全通过安全。第九届软件规范与设计国际研讨会论文集，1998年4月16-18日，日本伊势志摩（Isobe），第18-23页。IEEE计算机学会，1998年。[25] D. G. 韦伯 容错的形式规范及其与计算机安全的关系。ACM SIGSOFT Software Engineering Notes，14（3）：273
