160《理论计算机科学电子札记》66卷第2期（2002）网址：http://www.elsevier.nl/locate/entcs/volume66.html18页作为安全检查的活性检查Armin Biere，Cyrille Artho，Viktor Schuppan计算机系统研究所，ETHZentrumRZH，CH-8092Zürich，瑞士摘要时序逻辑被广泛用于指定硬件和软件系统。通常区分两种类型的属性，安全性和活性属性。虽然安全性可以很容易地通过可达性分析来检查，并且存在许多有效的安全属性检查器，但更复杂的算法一直被认为是检查活性所必需的。本文描述了活性检验问题到安全性检验问题的一种有效转换。通过将先前访问的状态保存在附加状态记录组件中并检查循环关闭条件来检测反例。该方法处理公平性，因此扩展到完全LTL。1介绍模型检测[12]是验证硬件和软件系统的时间规范的最成功的方法之一。系统属性在时态逻辑中被指定[13]，对于时态逻辑存在各种形式。通常有两种类型的属性，安全性和活性[19]。在实际应用中，安全性能是普遍存在的。因此，已经设计了非常有效的算法和工具来检查安全属性。大多数系统的规范仍然我们描述了一个通用的翻译过程，将一个具有活性指定的系统转换为一个新的系统，如果原系统中的活性属性成立，则该系统的安全属性是有效的。主要的动机是使现有的工具和技术，以检查活性，原本应该只对安全属性。例如，顺序ATPG（自动测试模式生成）[22]可以用于检查简单的时态公式类[3]，但一般的活性特性已经无法达到。这同样适用于STE（符号轨迹评估）[26，9]，尽管已经发布了一个可以处理所有ω-正则性质的STE的广义版本[27]。这两种技术已经在工业中使用了十多年[22，6]，并且存在有效的实现对于符号模型检查[21]，有大量关于仅适用于安全的优化的文献。边界集简化[7]，稠密2002年由ElsevierScienceB出版。 诉 操作访问根据C CB Y-NC-N D许可证进行。比耶尔，阿尔托，斯丘潘161¬[23]和优先级[8]的可达性分析都试图加速基于BDD的可达性计算，但迄今为止还没有适应于处理活性。前向模型检查[17，15，2]是通过仅访问可达状态并尽可能早地捕获错误来改进基于后向符号模型检查的尝试。它的动机是观察，检查安全属性的可达性分析。前向模型检查尝试专门使用前向图像计算。由于我们能够将活性转化为安全性，因此我们希望在不改变的情况下模型检测算法。Kupferman和Vardi开发了一种方法，通过搜索有限违反前缀来简化安全属性的基于自动机的模型检查[18]。通过我们的翻译，我们遵循类似的目标，将活性属性减少到安全属性，从而使更广泛的验证算法的应用成为可能。翻译是结构性的。它尊重系统的层次结构，可以很容易地应用，甚至手动，在设计入门级，如在硬件描述语言。 如果工具除了安全检查之外不包括其他模型检查算法，并且通常在商业环境中无法访问源代码，则这一点特别有用。其基本思想借鉴了显式的on-the-dry模型检查[14]和有界模型检查[1]：有限系统中活性属性的反例是套索形状，它由一个导致循环的前缀组成如在[1]主要的挑战是如何检测环路。在我们的翻译中，通过保存以前访问过的状态并稍后检查当前状态是否已经发生来找到。对于简单的活性属性，转换的结果并不比原始的模型检查问题大得多。我们还展示了如何处理更复杂的活性属性，例如涉及到until运算符。通过增加公平性约束，该技术可以扩展到全LTL。下一节详细介绍各种例子，以建立对翻译的直观理解。在第三节中，我们介绍了必要的正式背景。我们精确地定义了第4节中的翻译，证明了它的正确性，并比较了原始模型检查问题和最终模型检查问题的复杂性。在同一节中，我们提到了如何扩展我们的翻译来处理公平和LTL。第5节中的初步实验表明了我们的方法的可行性，第5节。6结束2直觉简单活性属性AFp的反例跟踪是一条无限路径，其中活性属性的主体p无处保持，或者等价地p沿着整个路径保持。迹线总是可以假定为如图1所示的套索形状。它由一个前缀组成，导致一个循环，从循环状态sl开始。从比耶尔，阿尔托，斯丘潘162¬` 阿姆斯壮Ks0s1slpppsl+1sk布雷普Fig. 1. AFp的一般套索形反例迹线。对于有限模型中的每一条无限迹线，我们都可以通过在一个状态第二次出现时立即闭合循环来构造一条套索形状的迹线。请注意，p仍然保持沿着构造的路径。这种观察是各种模型检查算法的核心。例子是布希自动机的显式状态算法[14]和有界模型检验中的展开活性性质[1]。有了这个限制，我们只需要寻找套索形状的反例。这在本文讨论的两种翻译中都有使用。第一个翻译，仅用于说明，被称为基于计数器的翻译。它扩展了公知的技术，只检查有界活性，但没有实用价值。我们的主要贡献是国家记录翻译。它产生一个状态机，可以在任何时候保存以前达到的状态。 两个transla-实例不仅修改了要检查的属性，而且还向模型添加了额外的检查组件，同时仍然保持互模拟等价性[12]。2.1基于计数器的翻译在模型检查应用中，经常观察到活性属性AFp可以通过在主体p必须保持的步骤数量上添加界限k来进一步限制。该界限在规范中给出，或者可以通过人工检查确定。有界活性属性AFkp定义为（一）AFkp<$A（p<$Xp <$···<$Xkp），其中Xip<$····X Xpi−times显然AFkp意味着AFp。如果边界选择得足够大，特别是与状态数一样大，则相反的方向也成立|S|在模型中，由于所有状态都是可达的，|S|步一个简单的转换只是将AFp与AFp交换，k是状态数。然而，（1）中AFkp的扩展导致非常大的公式，特别是在符号模型检查的上下文中。为了避免这种显式扩展，我们的基于计数器的翻译向模型添加了一个计数器，该计数器计算到目前为止达到的状态数。现在只需要检查，每当计数器达到原始模型的状态数时，发现p后一个属性可以通过在模型上附加一个布尔标记来检查，该标记会记住p在过去是否满足最后一步是依赖于属性作为第一个例子，我们使用初始状态为0的模4计数器。在图2中，示出了SMV程序[21]和计数器的状态图而比耶尔，阿尔托，斯丘潘163模块主VAR状态：-1.. 3;定义return = state =-1;分配intcount = 0;next（state）：=情况return 3：0 ;1：state +1 ;esac;发现规格AF图二、一个模4计数器，状态为-1。所有的状态都可以从-1到达，但是这个状态本身是不可到达的，因为计数器会返回到0。这个例子的状态空间包含五个状态。在五次转换之后，我们检查found是否从初始状态一直保持为false。 在这种情况下，找到了一个反例，否则，活性属性是有效的，因为每个长度为5的潜在套索形状的迹线都包含一个状态，在该状态下，发现成立。这允许将活性属性简单地转换为安全属性。该模型扩展了一个布尔变量live，它表示found是否已经为true。一个可变的计数器计算状态的数量图3的左列显示了转换后的规格。AF找到的live- ness属性转换为安全属性AG（finished->live）。这种翻译是非常不准确的，因为它总是需要穿越五个状态。2.2状态记录翻译代替在最坏情况下保守地搜索所需的时间，每当遍历先前看到的状态sl时，搜索应当终止。每次发现这样的循环时，活跃度属性p必须对之前访问过的至少一个状态保持否则，我们有一个反例（见图1）。因为状态空间遍历是无记忆的，所以没有办法显式地表示，一旦我们第二次到达状态sl，属性p新模型需要一种方法来由于我们事先不知道我们是否会在稍后再次看到当前状态，因此我们使用oraclesave来告诉模型当前状态是否被假设为循环的第一个状态。为了防止复制，使用另一个保存的变量在循环的最后一个状态sk之后，sl是再次遇到（见图4）。 此时，循环的谓词变为−10123比耶尔，阿尔托，斯丘潘164模块主VAR状态：-1.. 3;计数器：0.. live：boolean;定义return = state =-1;分配intcount = 0;next（state）：=情况return 3：0 ;1：state +1 ;esac;intcount = 0;下一个（计数器）：=情况计数器5：计数器+1;1：计数器;esac;intcount = 0;next（live）：=live|发现;定义finished：= counter = 5;SPEC AG（完成- >现场）(a) 计数器模块主VAR状态：-1.. 3;循环：-1.. 3 ;live：boolean;save：boolean;saved：boolean;定义return = state =-1;分配intcount = 0;next（state）：=情况return 3：0 ;1：state +1 ;esac;init（已保存）：= 0;next（已保存）：=救|保 存 ;next（loop）：=情况！save：state;1：循环;esac;intcount = 0;next（live）：= live|发 现 ;定义循环：=return loop;SPEC AG（循环- >实时）(b) 安全图三. 基于计数器的翻译和我们对活性属性的新翻译。p图四、循环检查AFp计数器示例作为可达性。为真，并且属性p必须至少被填充一次。如图所示4、循环关闭条件循环检查，当前状态是否已被访问相应地，图。图4示出了比图1多一个状态。因此，live和saved不应该指当前状态。它们的目的是记住found和save在过去是否特别是，它们的初始值应该为false。slslsls0S1SLsl+1SKsk+1 =比耶尔，阿尔托，斯丘潘165→⊆ ⊆×∈≤||||2.3将公平转化为安全公平属性也可以使用相同的方法进行转换。图5显示了一个示例，其中有两个任务t0和t1，每个任务从0到7计数。在每一步中，只允许一个任务轮流执行。活性属性，声明每个任务最终到达状态7，只有在以公平的方式进行轮流时才能被满足，即。每个任务最终都会轮到它为了在我们的例子中包含公平，我们定义了一个新的属性公平。它在每个循环中至少记录一次公平属性是否为真因为save和saved是全局的，所以它们与任务模块共享。3预赛我们的标记如下[12]。设A是一组原子命题。一个Kripke结构K，或者简单的模型，wrt。A被定义为K=（S，I，T，L），其中S一组有限的状态，IS一组初始状态，TS它的过渡关系，L：S2A为标号函数. 我们假设初始状态的集合是非空的，并且转移关系是全的，即对于每个状态s∈S存在一个状态SJ∈S，其中（s，SJ）∈T。当（s，SJ）∈T时，我们记T（s，sj），同样地，记I（s）。作为时态逻辑，我们使用CTL* 的子集，带有下一个时间操作符X和可能性操作符F。 我们不详细处理until操作符U或其他操作符，因为我们的翻译适用于包含这些操作符的完整LTL我们将只考虑通用路径量化器A.命题运算符是合取（conjunction）和否定（negation）。我们还添加了命题常量{0， 1}。CTL* 公式集由两类公式组成：路径公式Φ和状态公式Φ。所有的原子命题p A都是状态公式，它们总是可以被强制为路径公式。否定保持参数的类型。如果参数的类型匹配，这同样适用于合取。否则，它们的合取是一个路径公式。 时态算子应用于状态公式。路径公式可以由路径量化器预固定以获得状态公式。路径公式的语义定义为wrt。路，其中K的路的集合Π是所有有限和无限序列π=（si）的并集，其中si∈S和T（si，si+1）对于0i <π。π的长度π被定义为跃迁数。我们只考虑非空路径。我们将s i写成π（i），将序列（si+n）写成π n，其中ch与第一个n的原始路径相同国家删除。设p∈A，φ，φ1，φ2∈Φ，且φ1，φ2∈φ.的有效性比耶尔，阿尔托，斯丘潘166MONITORtask（id，turn）VAR状态：0..7 ;分配intcount = 0;next（state）：=情况turn = id状态7：state +1;1：状态;定义return = 7;公平turn = id模块主VARturn：0..1个;t0：task（0，turn）;t1：task（1，turn）;定义发现：= t0。找到了T1 发现;SPEC发现AFMONITOR任务（id，turn，save，saved）VAR状态：0..7 ;循环：0.. fair：boolean;分配intcount = 0;next（state）：=情况turn = id状态7：state +1;1：状态;定义return = 7;looped：=保存的状态=循环;分配intcount = 0;下一个（公平）：=公平|id = turn&（保存|已 保存）;next（loop）：=情况拯救！已保存：状态;1：循环;esac;模块主VARturn：0..1个;t0：task（0，turn，save，saved）;t1：task（1，turn，save，saved）;save：boolean;保存：boolean;live：boolean;定义发现：= t0。发现t1。找到;循环：= t0 .循环t1。循环;公平：= t0.公平t1.公平;分配intcount = 0;下一个（保存）：=保存|保存;intcount = 0;下一个（现场）：= live|发现;SPECAG（循环公平->现场）(a) 安全地生活图五、将具有公平性的活性分层转换为纯粹的安全性。比耶尔，阿尔托，斯丘潘167|∈∈ ∈∼∼ ⊆×s∈S和无穷大π∈S的状态和路径公式定义如下：S|=Aφiπ |= φ对于所有π ∈ Π，其中π（0）= sS |= p我的p∈L（s）S =100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000|伊什|=1和s |= 100S|=我的S |=π|= φ1φ2iπ |= φ1和π |= φ2π |=<$φ 我的π |= φπ |=F φi ≠存在i≥ 0且π i|= φπ |=X φ 我的π1|= φπ |=i π（0）|=我 们 还 将 使 用 其 他 布 尔 运 算 符 ， 如 析 取 （ disjunction ） 和 蕴 涵（implication）。全局时间算子G定义为Gφ<$$>F<$φ，存在路径量化器定义为Eφ <$$>A<$φ。路径π被初始化为wrt。给定模型K=（S，I，T，L）i <$π（0）I. 则CTL* 公式f对于所有初始化的无限路径π对Ki ∈ π = f有效。模型检验确定f对K的有效性。二次模型检验问题P=（K，f）和PJ=（KJ，fJ）等价于i <$K| = f惠KJ|= fJ.我们的翻译的前两个步骤节。4产生等效模型检查问题，通过互模拟等价性证明。在同一个原子命题集合上的两个模型K =（S，I，T，L）和KJ=（SJ，IJ，TJ，LJ）是互模拟等价的 ，且存在一个关系SSJ，具有以下性质：设S和SJSJ与ssJ。首先，标签比耶尔，阿尔托，斯丘潘168∈∼∈ ∼∈∈{|≥∈}| || || |匹配，即L（s）=LJ（sJ）。第二，对于所有的t S和T（s，t），必须存在tJSJ和TJ（sJ，tJ），ttJ。 最后，对于所有初始状态s，必须有一个初始状态IJ与ssJ。双重属性必须保持也对于简单属性（例如AFp和AGp），原始模型检查算法[11]的复杂度与模型K的大小呈线性关系。特别地，它与状态数S和跃迁数T成线性关系。 在On-the-Money模型检查[14]的情况下，复杂度可以进一步限制为与可达状态的数量成线性关系R与R=π（i）i0，πi，π i初始化。对于使用BDD的符号模型检查[21]，（可达）状态的数量不如定点迭代的数量重要。这个数由直径d限定，直径d被定义为两个状态s，t∈S之间的最大距离δ（s，t），其中δ（s，t）= min {k|π∈ π，|π|=k，π（0）=s，π（k）= t}在BFS可达性分析中，可以进一步限制迭代次数到所有可达状态到某个可能变化的初始状态的最大距离r，称为半径。在向后定点计算中，这是检查活性属性的传统方法，我们可以引入向后半径的类似概念，即到达定点后的向后迭代次数。后向半径不仅取决于模型，还取决于属性。注意，向后和向前半径是比耶尔，阿尔托，斯丘潘169⊥∼→⊥∼∼≤ ⊥◦没有关系。例如，当检查AGp时，归纳不变量p的后向半径为1，与模型的大小无关在实践中，纯向后模型检查通常优于前向模型检查[17]或反向模型检查的受限版本，其中定点计算中的近似被限制为预先计算的可达状态集。4翻译在这一节中，我们精确地描述了我们的状态记录翻译的抽象水平，并证明其正确性。具体的模型描述语言，如用于实验的SMV输入语言我们也不正式对待基于计数器的翻译。在本节的第二部分中，我们通过比较原始模型和翻译模型的尺寸和直径来讨论我们翻译的效率。在最后一部分中，我们描述了公平和LTL的扩展4.1正确性设K=（S，I，T，L）是一个Kripke结构，AFp是我们要检查的活性作为第一步，我们构造K=（S，I，T，L ），其中S=S×（S{}），I=I×{}。定义了新的过渡关系作为(2)T（（s，t），（sJ，tJ））惠T（s，sJ）（tJ=t（t=tJ=s））它像原始转换关系一样对第一个状态分量进行操作在第二状态分量中，先前到达的原始状态可以被记录，非确定性地，但最多一次（也参见图1A）。4）. 因此T在第二个状态分量中是单调的，其阶数≤S（S{}）2，其中stis= t或s=。新的标号是通过使用投影函数ρ对ρ（（s，t））=s的对进行运算得到的。我们进一步假设这是一个新的状态，它在S.本质上，我们的翻译模拟了K的原始行为，没有引入死胡同，保持了状态的标记因此我们在互模拟下，可以证明K和K是互模拟等价的∼ ⊆S×S⊥, withs∼s⊥⇔ρ(s⊥) = s.为了证明λ是互模拟，我们使用λλ：SS定义为λ（s）=（s，），并将λ和投影函数ρ以自然的方式映射到路径上。然后我们可以很容易地检查所有路径的π λ<$（π）和ρ（π<$）π<$这些函数为存在性量化器提供了必要的证人，是一种互模拟引理4.1 K和K是互模拟等价的。下一步添加一个标记，它记住p在路径上是否有效。结果是Kp=（Sp，Ip，Tp，Lp），其中Sp=S_p×{ 0， 1}，比耶尔，阿尔托，斯丘潘170→Ip=I<$×{ 0}，Tp（（s，x），（sJ，xJ））i <$T<$（s，SJ）<$（p∈L<$（s）→XJ=1）<$（p/∈L<$（s）→XJ=x）其余的定义为第一步。同样，Tp在第二状态分量中是单调的，在这种情况下，对于限制为{0，1}。注意，Kp取决于被检查的属性。与前面类似的推理，用稍微复杂一点的λp：S<$Sp和传递性论证给出了下面的引理。引理4.2 K和K p是互模拟等价的。由于CTL* 公式的有效性在互模拟等价性[4，12]下保持不变，我们得到了（K，AFp）与（Kp，AFp）的等价性.我们翻译的最后一步包括添加一个新的原子命题q，(3)q∈Lp（s，t），x））惠 s=t→x= 1这个定义表明了我们翻译的正确性定理4.3（K，AFp）与（K p，AG q）是等价的.证据有待证明的是EG<$p和EF<$q在Kp中的等价性。首先假设K p|=EG<$p. 则存在一条无限初始化路π∈Lp，其中p/∈Lp（π（i）），对所有i≥0。 由于Sp的状态数是有限的，所以必须存在指数k≥l≥0，其中π（k+1）=π（l）. 设π（i）=（（si，ti），xi），其中i≥0，定义πJ（i）=（（si，tJi），xi），其中tJi=0，0≤i≤l和tJi=sl，其中l i≤k+1。显然，πJ是K p的初始化合法路。 通过定义we有sk+1=tJk+1=s l和x i= 0（0 ≤i≤k+1），因为p/∈Lp（πJ（j））=L（s j）= Lp（π（j））（0≤j≤k）。从（3）我们得到q/∈Lp（πJ（k+1）），并且πJ证明是EF<$q的证明，假设πJ以明显的方式扩展到无限路。注意Tp是全的，因为我们的翻译没有引入死胡同。对于相反方向，假设EF<$q成立。在不失一般性的情况下，我们找到一条初始化路径π ∈ Π p，|π|= k +1和π（k +1）|=<$q. 当π（i）=（（si，ti），xi）时，我们从（3）推出sk+1=tk+1和xk+1=0. From的单调性，我们得到了一个l，0 k，则定义tJi=tk+1，xJi=xk+1，sJi=sl+c，其中c=（i−l）mod（k +1 −l）。从Tp在其第二个周期状态分量，我们有x k+1=. = x0= 0，这意味着s i|=P，0≤i≤k。由于这些原始状态决定了p对每个πJ（i）的无效性，并且πJ是在有限路径上合法初始化的，它可以作为EG<$p的证明。4.2复杂性我们的目标是使用以前仅用于可达性计算或安全检查的技术和工具来检查活性属性。的比耶尔，阿尔托，斯丘潘171∨ ⊥∧·| |||联系我们||·我们的翻译对模型检查或可达性计算的复杂性的影响是相当合理的。如图1的示例所示5、程序代码中非规范符号描述的大小，只增加一个小的基于计数器的翻译将产生非常大的反例。因此，我们将讨论限制在状态记录翻译。在全局（显式）模型检查[11]中，复杂度由状态的数量决定，状态的数量以二次方式增加：|= 2·|S|= 2·|S|·（|S |n = O（|S|（二）|2)在直接（显式）模型检查[14]的情况下，只关心可达状态空间Rp的大小。K的可达状态（s，t）∈R要么包含k作为第二个分量t，要么t在K中可达，因为只记录可达状态。因此R由R（R+ 1）有界。 这个界限是紧的：一个模n计数器，如图2中n= 4的模型，有R=n（n+ 1）个可达状态。 如果n = 4，则0，.， 三，零，... 3可以到达。进一步介绍p-记录最多可以将数量翻倍：|≤ 2·|R|≤ 2·|R|·（|R |n = O（|R|（二）|2)关于BDD的符号模型检查[21]，我们有两个结果。第一我们将约化有序BDD的大小与K，K_p和K_p的跃迁关系联系起来。假设S用n =[log 2]编码|S||状态位，我们可以用2 n +1个 布尔变量对S进行编码。重要的是要将第一个和第二个组件的布尔变量。否则（2）中的项（tJ=t（t=tJ=s在交错阶的情况下，它在n中是线性的，因子约为十一岁该因素具有对于大的状态空间是凭经验确定的。因此，通过使用[5]中的事实，即在BDD上计算任何布尔二进制运算将产生BDD的大小与自变量BDD的大小的因子1成线性。最后，与针对Tp的BDD的大小相比，针对Tp的BDD的大小可以增加表示Tp的集合的BDD的大小的线性因子。p成立的状态，实际上通常很小。对初始状态集合的类似计算表明，表示Kp的BDD的大小可以被约束为在表示K的BDD的大小上是线性的，在状态位的数量上是线性的，并且在表示p保持的状态集合这些静态边界并没有说明定点迭代中BDD的大小。为了测量动态复杂度，我们确定直径和半径的界限，这也是定点迭代的最大次数的界限。注意，基于计数器的转换具有至少与原始系统中的状态的数量一样大的半径，这使得传统的符号可达性比耶尔，阿尔托，斯丘潘172⊥≤··−⊆| |∞即使对于中等规模的问题，分析也不切实际。一个重要的观察结果是，状态记录平移产生小得多的直径dp和半径rp：定理4.4dp≤4·d +3和r p≤r +3·d +3证据 设π∈π是一条满足π（i）=（si，ti）的有限路，|π|= k。 由于T在第二分量中是单调的，我们必须区分两种情况。如果第一个t0=... =tk，则δ（π（0），π（k））=δ（s0，sk）≤d，因为K中的所有路都可以通过添加固定不变的第二状态分量而扩展为K中的在第二种情况下，存在一个l，其中0≤lk如果t0=…= t l=和t l+1=... =tk=sl（参见图4）。现在，我们有两个子路径，与第一种情况一样，具有恒定的第二状态分量，并获得δn（π（0），π（k））≤δ（s0，sl） + 1 +δ（sl+1，sk）≤2·d+ 1这也包含了第一种情况的界限，因此d=2d + 1。为了确定半径的界限，我们还假设π被初始化。则δ（s0，sl）≤r，得到rl≤r+d+1.同样的道理，因为Tp在第二态分量上也是单调的，我们得到dp≤2·d∞ +1且rp≤rn+dn+ 1。 通过代入，我们得到所需的不等式。✷不幸的是，有一些例子中r比d小得多，对于Kp中的可达性分析，我们仍然需要执行比d固定点迭代更多的迭代。如果我们允许所有的状态都是初始状态，那么图2中没有-1状态的模n计数器就是这样一个例子。则我们有d=n− 1，r= 0，但d=2 n 1且r= n，它已经大于d。中检查活动性属性所需的向后迭代次数原始模型也可以非常大。4.3公平和LTL我们的翻译能够体现公平。公平性约束仅仅是S的子集。路径π称为公平wrt。一个公平性约束Fi Si在Fi中的某些状态在π上无限频繁地出现。如果π是公平的，那么π是无限的，写为π=. 形式上，我们向模型中添加一个公平性分量F，其中F是公平性约束F =（F1，...，F m）。 那么一条路对K来说是公平的，它是公平的。每一个Fi。具有公平性约束的模型的语义定义与不公平的情况相同，只是所有路径都需要公平。具有公平性的互模拟是通过将上述基于转换的定义扩展到整个公平路径来定义的，如[12]所示：条件是对于所有的公平路径π∈Π j，存在一个公平路径πJ∈ΠJ，π <$πj，其中π<$πJi <$π（i）<$πJ（i），对于所有i≥0。为了处理公平的Kripke结构K（S，I，T，L，F），我们构造Kp（Sp，Ip，Tp，Lp，Fp），其中Sp，Ip，Tp，而P和L的定义如上所述，F被扩展为F p=（F1×（S {}）× {0，1}，...，F m×（S <${0}）× {0，1}）。比耶尔，阿尔托，斯丘潘173ppp∈ ∈{}pppppppppp我们定义KF=（SF，IF，TF，LF），其中SF=Sp× { 0， 1} m，IF = Ip × { 0，1 }m{（0，.，0）}的状态比特来替换每个公平性约束Fi，记住Fi中的循环状态是否已达到。设LF为Lp的自然延伸。设（s，t，x，v），（sJ，tJ，xJ，vJ）∈SF，其中s，sJ S，t，tJ S，x，xJ0，1和v，vJ0，1 m。转换关系TF满足（s，t，x，v）和（sJ，tJ，xJ，vJ）作为当前和下一状态我的Tp（s，t），x），（（sJ，tJ），xJ））mi=1 （vJ（i）=v（i）<$（tJ/=<$$>s∈Fi<$vJ（i）=1））其在状态空间的新公平性分量中再次是单调的我们进一步增加一个新的原子命题qF，q F∈L F（s，t，x，v））惠（v（1）=. =v（m）= 1）→q∈Lp（（s，t），x）其中q被定义为Kp。我们可以像以前一样证明正确性结果，现在包括公平性。定理4.5（K，AFp）和（KF，AG q F）是等价的.所添加的状态比特的数量在公平性约束的数量m中线性增长。这直接对应于输入大小的增加，符号模型检验 状态空间KF自身呈指数增长。所以计算直径和半径。该方法似乎是可行的，至少对于显式模型检查，只有少量的公平性约束。然而，检查AGqF总是会找到最短的反例。另一种方法是计算满足的公平性约束的数量，类似于众所周知的将广义Bu？chi自动机i n转换为普通Bu？chi自动机。 它提出了一个具有单一公平性约束的活特性，而公平性约束又转化为安全性。这种方法更节省空间。它只需要对数附加状态位。然而，它无法生成最小长度的反例轨迹。 此外，还不清楚这种二进制编码与之前讨论的独热由于广义Bu¨chi自动机和LTL[14]都可以转化为公平的Kripke结构，因此我们的转化也适用于一般的LTL模型检测。此外，还可以为其他标准LTL运算符导出特殊的转换规则。例如，为了处理p1Up2，我们使用p1Up2<$（p1U弱p2）<$Fp2其中弱直到算子p1Uweakp2被定义为对路径i有效，p1不会在p2保持之前停止保持，或者p1沿着整个路径保持。通过添加一个状态位来记住p2是否已经充满，弱直到可以很容易地转换为简单的安全属性。则比耶尔，阿尔托，斯丘潘174检查真检查错误反例假n生活计数安全生活计数安全生活计数安全48（4+4）9（9+0）8（8+0）5（4+1）5（5+0）4（4+0）7（3+4）5（0+5）4（0+4）816（8+8）17（17+0）16（16+0）9（8+1）9（9+0）8（8+0）15（7+8）9（0+9）8（0+8）12二十四（十二+十二）25（25+0）24（24+0）十三（十二加一）十三（十三+零）12（12+0）23（11+12）13（0+13）12（0+12）1632（16+16）三十三（三十三+零）三十二（三十二+零）十七（十六+一）17（17+0）16（16+0）31（15+16）17（0+17）16（0+16）表1计数器Fp2也被转化为安全性质，与我们的原始翻译一样。最后，我们同时检查两个安全属性。5实验在本节中，我们将展示我们的翻译结果应用于各种示例，包括理论和“现实世界”的示例。每个表分为三个主要部分：左边部分，正确模型所需的迭代，中间部分，模型不正确，右边部分，显示计算不正确模型的反例所需的迭代。对于每种不同的方法，三个主要部分被进一步分成一列：live用于传统的活性方法，count用于基于计数器的方法（未在FireWire示例中使用），safe用于我们的状态记录转换。对于每个版本，将显示总迭代、正向迭代和反向迭代的次数。5.1简单计数器在表1中的简单计数器的情况下，所有方法在迭代次数wrt中线性地执行模型尺寸。然而，计算反例所需的迭代次数几乎是实时版本的两倍，而不是我们的方法。对于表2中使用的计数器，可以在一个步骤中从任何状态到达期望状态n。只需要两次迭代就可以完成一个循环，并且需要n次向后迭代就可以到达所有可能的前导。利用基于计数器的方法，需要n+ 1次迭代来枚举足够的状态，并且需要另一次迭代来达到状态n。我们的方法需要恒定的五次迭代来获得正确的模型：一次迭代到达所有可能的后继状态;从这些状态开始，第二次迭代到达状态n。第三次迭代再次到达初始状态0，从那里需要两次迭代来证明循环内的活性错误的例子需要两次循环迭代，而在实时版本中，另一次反向迭代将初始状态作为前驱。基于计数器的方法是非常低效的。反例分析显示了类似的行为。比耶尔，阿尔托，斯丘潘175检查真检查错误反例假n生活计数安全生活计数安全生活计数安全46（2+4）6（6+0）5（5+0）3（2+1）5（5+0）2（2+0）3（1+2）5（0+5）2（0+2）810（2+8）10（10+0）5（5+0）3（2+1）9（9+0）2（2+0）3（1+2）9（0+9）2（0+2）1214（2+12）14（14+0）5（5+0）3（2+1）十三（十三+零）2（2+0）3（1+2）13（0+13）2（0+2）1618（2+16）18（18+0）5（5+0）3（2+1）17（17+0）2（2+0）3（1+2）17（0+17）2（0+2）表2跳过计数器5.2IEEE 1394火线IEEE 1394（火线）[16]是一种串行高速总线协议，广泛用于多媒体设备和PC的互连。为了确保协议的正确运行，连接到IEEE 1394总线的节点需要形成树。每次总线配置发生变化时，都会执行树识别协议，以验证此条件，并选出一个唯一的领导者，该领导者在协议的后续阶段具有扩展的责任。在以前的工作[25，24]中，我们已经验证了SMV树识别协议的几个属性在树识别阶段中要验证的最重要的一个属性是在到达协议的下一个阶段之前指定一个领导者。在我们的实验中，对[24]中模型的原始（正确）版本和具有阻止协议成功完成的错误的版本都检查了此属性。在SMV输入语言中，它针对2个节点公式化如下AF（node[0].根|节 点 [1]。根|超时|已 知 问题）其中root、超时和已知问题是状态属性。使用单独的安全属性来确保没有发生超时或已知问题一旦得到验证，这些条件可以从模型中删除，并且不包括在此处给出的性能数据中。在协议运行期间，两个节点可能会竞争成为根节点。在这种情况下，调用一个子协议来解决这种情况，称为根争用。两个竞争节点都非确定性地选择在继续之前等待短时间或长时间。如果选择不同的节点，其中一个将成为根。否则，重复子协议。公平性条件确保两个节点在某个时刻会做出不同的选择。第4节所述翻译过程的大多数步骤已实现自动化。对于翻译，使用NuSMV [10]生成一个可扩展的模型。引入了额外的变量来记录保存的状态， Oracle，并跟踪每个公平性条件在循环中是否为真。AF p形式的简单活性属性也会自动转换。更复杂的属性需要由用户通过使用基于自动机的方法或通过简单的变换比耶尔，阿尔托，斯丘潘176检查真检查错误假CEXnp生活安全生活安全生活安全2274 (19+55）24 (24+0）34 (19+15）13 (13+0）132 (13+119）13 （0+13）2374 (19+55）24 (24+0）35 (19+16）13 (13+0）132 (13+119）13 （0+13）2478 (19+59）24 (24+0）36 (19+17）13 (13+0）132 (13+119）13 （0+13）3276 (21+55）23 (23+0）36 (21+15）11 (11+0）67 (10+57） 11 （0+11）3377 (21+56）23 (23+0）37 (21+16）11 (11+0）67 (10+57） 11 （0+11）3477 (21+56）23 (23+0）37 (21+16）11 (11+0）67 (10+57） 11 （0+11）42129 (31+98）36 (36+0）52 (31+21）19 (19+0）215 (19+196）19 （0+19）表3树识别协议中的Leader选举-迭代检查真check + cex false生活安全生活安全np时间存储器时间存储器时间存储器时间存储器220.85669414.193970301.121032992.64282859231.9320168011.077825742.652151696.82595756244.7144394728.2212960885.4540253516.009444823211.3369922239.4519468667.5971891012.097725083376.053777278283.07957824253.60367867686.82421792534450.72292205421567.6731759998259.5119588279554.391436465042357.30140016931376.1835547502204.8212500473644.1824864717表4树识别协议中的Leader选举类似于我们在4.3节中给出的until运算符。最后，生成一个改进的变量阶。为了进行公平的比较，在检查之前也对现场模型进行了检查。我们在运行Linux 2.2.19的Pentium III-800上使用Cadence
我的内容管理
展开
