电子笔记在理论计算机科学50号4（2001）。VEPAS 2001网址：http://www.elsevier.nl/locate/entcs/volume50.html14页Futurebus+ Cache一致性协议马塞尔·基亚斯计算机科学与应用数学研究所，Christian-Albrechts-Universitat，D-24105 Kiel，德国，mky@informatik.uni-kiel.de摘要在本文中，我们描述了一个网络不变量的所有配置的未来总线+缓存一致性协议。用PAX计算网络不变量，并用模型检测器进行验证。使用这个不变量，我们能够证明一个规范的高速缓存一致性正确的任意数量的组件在一个单一的总线上的系统。此规范包括尚未证明的进度属性。 我们展示了如何单总线系统的结果可以扩展到树形系统。据我们所知，这是多数据总线协议的第一个统一证明。1介绍参数化网络的自动或半自动验证，即，系统族P = fPi j i 2！g，其中每个Pi是由i个过程组成的网络，是一个有趣而困难的任务：[2]证明了参数化网络的验证问题一般是不可判定的。然而，自动和半自动方法的veri-已经开发了参数化网络的限制类的阳离子例如，在一个实施例中，[21，29，16，23，1，7，5]。这些方法尚未应用于真实世界的示例。我们证明，WS1S转换系统的抽象方法[3，4，5]可以应用于Futurebus+ Cache Coherence Protocol [19]。在IEEE Futurebus+协议的验证中投入了大量的精力[11，6，20，12]。或者这些努力没有提出一个统一的正确性证明为参数化网络的所有实例建立正确性的证明，或者它们仅验证了高速缓存一致性规范的子集。c 2001年由Elsevier Science B出版。V.CC BY-NC-ND许可下的开放访问。VEPAS 2001 {M.基亚斯2我们的证明方法基于[3，4，5]中描述的方法。它包括在一个后继者的弱二阶逻辑（WS1S）理论[8，15，28]中建立参数化网络的模型。动态行为描述了WS1S过渡系统。在WS1S中建立了一个抽象关系。两者都作为工具PAX的输入，PAX计算使用MONA从模型中抽象出nite-state系统[18]。 所得抽象系统适合作为符号模型检查器的输入[26，10，12]，该符号模型检查器验证规范。我们的规范是在线性时序逻辑（LTL）[25]中给出的。它可以使用模型检查器NuSMV [9]进行检查。在[3，4，5]中，并行组合是异步的，即，基于交互语义学。为了处理Futurebus+协议的体系结构，我们扩展了同步并行组合的方法。使用这种方法，我们证明了协议正确的高速缓存一致性，其中包括一个进步的属性，这尚未在文献中得到证明此外，通过使用组合推理，我们证明了协议正确的树结构。路线图在下一节中，我们将介绍本文中使用的符号和定义。我们回顾了WS1S转换系统的定义。第3节描述了我们将文[3，4，5]中的证明方法推广到同步并行合成。Futurebus+ Cache Coherence Protocol的简短描述在第4节中给出。第5节回顾了L-模拟和网络不变量的定义，总结了[22]的结果，并描述了一般情况下网络不变量的构造。我们结束这篇文章的一个简短的结论和比较相关的工作。2预赛在这一节中，我们简要回顾了WS1S [8，15，28]和布尔转移系统[3，4]的基本定义。WS1S的项是从常量0、一阶变量和应用于项t的后继函数t：t+ 1构建的。二阶项是二阶变量，常数;表示空集，或形式为X[X 0，X\X 0，orXn X 0 的 项，其中X和X 0表示二阶项。 拓扑公式的形式为 b，t=t0，0其中[=]是替换操作，k是同步并行com。位置SMPS可以表示为WS 1 S转换系统（WS 1 S-TS）。定义3.2WS 1 S过渡系统S=（; V; T）由下式定义：V是一组二阶变量，其中每个变量都被解释为作为 自然数的集合。初始条件由一个满意的断言给出关于FV（）V.T是一组跃迁，其中每个跃迁由WS 1 S公式（V;V0）表示，其中F V（）V[V0]。S的计算是状态序列，并按通常定义。通过以下转换过程将SMPS转换为双相似WS 1 S-TS：设P=f1，n g是从1到n的过程索引的集合。 我们使用一个平移函数，它将所有出现的n替换为max（P）+ 1。同品种部分（P; B）=（^B;B02B^B6=B0B\B0=;）^[B=PB2B确定集合系统B是否是集合P的划分。翻译程序为：定义3.3考虑由S（i; n）=（;V; T）构建的SMPS P。则WS 1 S-TS（~;V~;T~）由下式定义：当P=62V时，V~=V[fPg]。Let~=9n：P=f1; ： ：;n g ^ 2 （VB2VBP）^（8Pm：）.设T~=f~g，其中e~=92 TY：部分（P;fY j2T g）^（VB2VBP）^（P = P0）^（82Ti：V2T （i2Y！ [i=i2Xp]））和i2f1;：;ngxiabb reviatesx1：x2：xn：for2f8;9g.转换关系仅由一个公式给出然而，计算WS1S公式的模型集所需的空间一个2的幂的叠的长度的大小的公式[27]。 在我们的案例研究中，这导致了一个公式，这个公式太大了，无法用我们的资源来处理。这使得有必要保持过渡关系的公式很小。在[22]中，提出了一种补救这种情况的方法。4Futurebus+ Cache一致性协议本节的目的是概述IEEE未来总线+协议[19]的工作原理。一个缓存必须是一系列所谓的缓存VEPAS 2001 {M.基亚斯5next（cmd）：= casestate=invalid：{none，read-shared，read-modified};state=shared-unmodified：{none，invalid，read-shared，read-modified};state= exclusive-modified：{none，copyback};state=exclusive-modified：{none，copyback};esac;图1.一、缓存行命令部分的SMV代码线该标准的一部分是设计用于分层结构多总线系统的高速缓存一致性协议。该协议通过让高速缓存窥探或观察所有总线事务来保持各个总线上的一致性。跨总线的一致性使用总线桥来维持。特殊代理，称为缓存和内存代理，在桥的两端代表远程缓存和内存。为了提高性能，该协议使用所谓的分割事务。当一个事务被拆分时，它的完成被延迟，总线被释放;在稍后的某个时间，发出一个显式响应来完成事务。该功能使得在处理远程请求的同时为本地请求提供服务成为可能。高速缓存行的状态由四个属性invalid、shared-unmodi ed、exclusive-modi ed和exclusive-unmodi ed表征。图1显示NuSMV语法中系统的命令部分[9]。以下段落对所有过渡进行了非正式概述。事务是总线上的一系列事件。基本上，它是一个总线命令，它描述了事务的性质。总线命令的确切语义可以由总线属性IV、SR、TF或WT中的一个来修改。每个处理器都有这些属性的本地副本，分别称为iv、sr、tf或wt。通常，如果设置了这样一个属性的本地副本，它也会通过或（_）操作在总线上设置最初，任何高速缓存行都是无效的。一个无效的缓存行必须发出一个命令或捕获一个所需数据的副本来改变其状态（捕获意味着从另一个组件发出的事务中读取数据）。高速缓存行可以从无效状态转换到任何其他状态。如果TF被断言，则发起读共享事务并成功完成该读共享事务的模块转换到共享未修改状态，否则转换到独占未修改状态。它可以在读共享、读无效或复制回事务期间断言tf以将其状态改变为共享未修改。启动成功完成的读修改事务的模块将使其高速缓存行将状态改变为独占修改。如果高速缓存行处于共享未修改状态，则其可以在任何时间将其状态改变为无效状态而无需总线事务。 如果它窥探到读修改、写无效或无效事务，则需要这样做。如果它窥探到一个读无效或读共享事务，并且没有断言tf来snarf数据，它也会将状态更改为无效一种启动失效的模块VEPAS 2001 {M.基亚斯6成功完成的事务将状态更改为exclusive-modi ed。否则它不会更改状态。在不使用任何总线事务的情况下，处于独占未修改状态的模块可以在任何时间将其状态改变为其他三个状态中的任何一个。如果它监听读共享或读无效事务，则在此期间它断言tf，否则将状态更改为shared-unmodi ed和invalid。 如果它窥探到读修改的、写无效的或无效的事务，则需要这样做。处理器可以通过发起回拷事务来将处于独占修改状态的高速缓存行的状态它必须断言tf以将状态更改为shared-unmodi ed。如果此模块侦听到读共享、读无效或读修改的事务，则它必须断言iv以进行干预并提供数据代替内存。如果它在读共享或读无效事务期间断言tf，则它可以保留共享未修改的副本。如果它窥探到写无效事务，它总是将缓存行的状态更改为无效。对于WT被断言的任何命令，高速缓存行不应改变其状态。此外，如果模块的访问时间与总线访问时间相比慢，则模块可以拆分事务。高速缓存和内存模块通过解码它们窥探的每个高速缓存一致性读取事务的地址和命令来确定它们是否需要拆分事务如果模块负责该地址，并且不能立即响应，则断言sr。如果一个模块拆分一个读共享或读无效事务，它最终必须响应一个共享响应事务。该事务可能被任何缓存所阻塞。内存必须从这个事务中提取数据。如果没有其他高速缓存发出信号表示它具有高速缓存行或者它正在通过在共享响应事务上断言tf来捕获数据，则请求者可以将该行标记为独占未修改。否则，它是共享的。如果一个模块拆分一个读修改的事务，它最终必须用一个修改的响应事务来响应。这笔交易可能不会被扭曲。最初生成读取修改或无效事务并且随后接收到修改响应的模块将其高速缓存行状态改变为独占修改。如果任何其他模块向同一缓存行发起请求事务，则拆分事务的模块需要断言wt。 这强制限制了每个缓存行的单个未完成事务。当发起事务的模块接收到等待状态时，它必须等待，直到高速缓存行观察到共享响应或修改的响应，然后它可以重复其请求。在共享响应事务的情况下，它可以在没有总线事务的情况下对数据进行分割并满足其请求VEPAS 2001 {M.基亚斯7一致性协议。 设v表示，是一个L-模拟[14]和v缓存一致性。我们基于[11，12]的高速缓存一致性规范。其中一个规范被带有公平性假设的进度属性所取代。为了做到这一点，规范被重写为LTL [25]。在[19]中，指定了非法的属性组合。每当观察到这样的组合时，系统就会设置总线错误。即使所观察到的交易是合法的，它也可能指示错误。不存在这些错误条件被指定为（1）。接下来，我们希望最多有一个处理器，索引为i，有一个可写的缓存行;这由（2）表示。如果任何缓存行i和j都有一个处于可读状态的缓存行，我们要求它们在数据上达成一致。如果高速缓存行i持有可读副本，并且已知存储器行未被修改，则两者应该在数据上一致（参见（3）和（4））。公平性假设表明总线上的每个成员将经常是总线的主设备，经常在总线上发出命令，并且等待属性不是持久的，如（5）所表示的。在这个假设下，我们要求如果一个处理器正在等待一个请求，它最终会收到一个应答。此外，如果组件有义务响应请求，则它最终将履行其义务，如（6）和（7）所表达(1)2：（bus-error_error）(2)8i：8j：i6=j！ （2pi：写eable！：（pj：readable_pj：writeable））(3)8i：8j：i6= j！（2 p i：readable ^p j：readable！ p i：data = p j：data）(4)8i：2pi：readable^：m：memor y-lin e-m odied！pi：data=m：data（5）=（8d：d2D！23d：主）^（23CMD6=非e）^（23：WT）(6)8i：！ 2（p i：请求者6=无！3（p i：请求者=无））(7)8i：！2（p i：响应者6=无！3（pi：应答者=无））5未来总线+的网络不变量目前还没有人为Futurebus+ Cache提出正确的网络不变量L L存在L模拟。 然后，形式化地定义了网络不变量通过：定义5.1Let（P;vL）是一个局部或绝对的过程集，并且k单调，其中r∈vL，即，对于一个llP;Q2P，PvL 对于11R2P，我们有PkRvLQkR.然后，如果对于一个P2 P，它满足PvLI和PkIvLI，则我们将在nvariaVEPAS 2001 {M.基亚斯8n t中计算一个过程I2P。一个网络不变量是一个抽象的所有成员的家庭[29]，并通过这一点有：定理5.2设I是P的网络不变量，一种规格。如果VEPAS 2001 {M.基亚斯9I j= ，则对所有的P2 P，我们有Pj =.根据这个定理，找到一个网络不变量是足够的，它满足一个性质，表明这个家族的所有成员都具有这个性质。不幸的是，发送网络不变量是一项艰巨的任务。有人可能会问，这样的网络不变量是否总能找到，甚至是否可以自动计算。事实上，确定一个网络不变量是不可判定的[29]。5.1Futurebus+单总线网络在本节中，我们将描述如何为Futurebus+系统的单总线配置构建网络不变量。在[12]中可以找到一个非常相似但错误的网络不变量。5.1.1建立参数化模型构造网络不变量的第一步是将协议的参数化模型定义为WS1S转换系统。在这种特殊情况下，这是一项简单的任务。我们使用了[11]中描述的模型，并将其转换为BTS（见定义2.1）。使用第3节中描述的方法，我们已经从这个描述中构建了一个WS 1 S-TS。 模型中没有考虑存储器线和总线本身。它们是手动添加到WS 1 S-TS的。为了最小化WS 1 S-TS，已经投入了大量的精力。从系统的WS1S描述构造的自动机的转移关系可以在系统的描述中出现的变量的数量上呈指数增长。因此，我们尽量减少二阶变量的数量和转换关系的语法表示。这在[22]中有详细描述。5.1.2找到抽象关系我们的网络不变量是使用手动提供的抽象关系从WS 1 S-TS自动计算的：I$（8i：pi：state = invalid）^SU$（8i：pi：state = exclusive-modi ed^pi：state 6= exclusive-unmodi ed）^EM$（9i：p i：state = exclusive-modi ed ^8j：i 6= j！ p j：state = invalid）^EU$（9i：p i：state = exclusive-unmodi ed ^8j：i 6= j！ p j：state = invalid）^BAD$：（I_ SU _ EM _ EU）_ bus-error _ error：这是抽象关系的“自然选择”。这个想法是，抽象过程应该能够“模VEPAS 2001 {M.基亚斯10仿”它所抽象的系统的每一个行为。同样的想法也在[12]中使用我们介绍一个抽象的VEPAS 2001 {M.基亚斯11LLLi d，S1vS2，以及S1vS3。 那么S1kS2vS2kS3.next（cmd）：= casestate=invalid：{none，read-shared，read-modified};state=shared-unmodified：{none，invalid，read-shared，read-modified};state=exclusive-unmodified：{none，copyback，read-shared，read-modified};state=exclusive-modified：{none，copyback，read-shared，read-modified};esac;图二.网络不变量命令部分状态BAD，其观察对规范（1）和（2）中定义的安全特性的任何违反。抽象系统的命令部分如图2所示。它与原始系统的区别仅在于系统发出下一个命令的方式。通过比较图2至图1、这些变化变得明显：在独占修改和独占未修改中，可以发起读取修改和读取共享事务。如果高速缓存行处于共享-未修改状态，则其可以发出读取-修改和读取-共享命令。下一步是证明这样构建的系统是否确实是网络不变量要做到这一点，我们必须检查系统抽象系统和抽象关系是否满足Def。5.1.第一个要求（PvI）成立，如果抽象关系暗示身份关系，即， ID得双曲余切值.是S（0; 1）的状态集合。为第二个要求（P k IvI），我们可以利用平行线这里使用的复合操作为我们提供了交集语义（参见[22]关于该状态的部分），即，[[PkI]]=[[P]]\[[I]]=[[P]]，be原因id. 最后，我们必须检查并行组合操作相对于我们的抽象关系是否确实是单调的。 幸运的是，这是事实，正如下面的引理所述引理5.3LetS1 =（1;V;T1），S2 =（2;V;T2），且S3 =（3;V;T3）beBTS，Si对于i2f1;2;3g的状态集，一个抽象动作，使得L L L我的律师。 因为id声明等于[[S1]]\[[S2]]\[[S3]]。由S1vS2wehave[[S1]]\[[S2]]=[[S1]]。从[[S1]][[S2]]和[[S1]][[S3]]我们有[[S1]]\[[S1]][[S2]]\[[S3]]，从该权利要求书中可以看出。因此，在我们的框架中，为了计算网络不变量，抽象关系只需要包含参数化系统和抽象之间的身份关系。注意，抽象系统没有达到状态BAD，即，该图立即显示了说明（1）和（2）的有效性。VEPAS 2001 {M.基亚斯12next（cmd）：= casestate=invalid：{none，copyback，read-shared，read-modified}; state=shared-unmodified：{none，invalid，copyback}; state=exclusive-unmodified：{none，copyback，read-shared，read-modified};state=exclusive-modified：{none，copyback，read-shared，read-modified};esac;图3.第三章。命令部分的SMV代码[1]原因如下：回想一下图1中的处理器如何发出下一个命令。假设高速缓存行处于独占修改状态。例如，处理器不能发出read-shared命令。这可以通过两个处理器配置来完成，其中第二个处理器处于无效状态。5.1.3比较[12]。在[12]中，提出了一个系统，作者声称它是Futurebus+ Cache CoherenceProtocol的网络不变量。其命令部分如图3所示。它不是网络不变式，因为：在无效状态下，不应该启动回拷事务，因为它的数据是无效的。这样的事务使存储器行的内容无效。此外，如果该模型中的高速缓存行处于共享未修改状态，则不允许该高速缓存行发出任何读取命令。如果考虑处于共享未修改状态的系统并将其与处于无效状态的高速缓存行组合，则[12]中的系统不是该系统的抽象，因为它不能模仿由无效高速缓存行发出的读取命令。5.1.4验证图2中的网络不变量满足第4节的规定。用PAX和NuSMV建立了证明所涉及的计算花了不到2分钟。规范（6）和（7）需要特殊处理，因为任何读事务都可能被拆分。这将导致一个使该规范无效的计算，其中事务总是被拆分。利用文献[4，5]中的一个证明规则，我们可以证明系统满足2 3：SR。因此，我们建立了所有单总线配置的规范。5.2概括结果在本节中，我们将描述如何将结果从线性情况推广到任意网络拓扑。一般情况下网络不变量的构造基于以下两个观察：(i) 内存板和内存代理具有非常相似的行为。如果考虑总线上存储器代理的通信VEPAS 2001 {M.基亚斯13不能将其与存储器板区分开（这是其设计的意图）。我们可以展示给你看 M，其中MA表示内存代理，M表示内存板。(ii) 处理器和缓存代理也有非常相似的行为。作为一个例子，我们有一个CAvLP，其中CA是缓存年龄nt和P的处理器与其缓存线。使用这些抽象和事实，我们的平行组成是单调的，相对于vL（参见[22]）所讨论的网络变量对于单总线情况（RF.第5.1节）。这一点将在以下各段中予以确定。第一步是显示总线桥BB不干扰正常操作。在我们的协议模型中，总线桥本身有一个即时的传输时间，只传输最必要的行为。消息传播所引入的延迟是通过让代理在其本地总线上非确定性地拆分读取命令来模拟的 那么很容易看出，BBvLB，其中B是数据总线。我们已经说过，MkBkPvL 我，我是新的工作。使用k的单调性y，相对于vL 以及vL 是transitive，一个有MAkBBkCAvLMkBkPvLI。第二步是把这些结果放在一起。单总线系统由数据总线、存储单元和任意数量的处理器组成。 通过抽象MAvLM，可以用内存代理替换总线上的内存单元，而不改变其行为。类似地，任何处理器都可以被高速缓存代理替换。 于是，公交车变成了 树节点。主要的一点是，这些替换中的任何一个都具有相同的网络不变量，因为内存代理和缓存代理是存储器或高速缓存的实现，并且每个代理表示总线上的因此，我们已经证明：命题5.4I是Futurebus + Cache Coherence Protocol的任何配置的网络不变量。这为将来总线+高速缓存一致性协议的所有拓扑结构的规范提供了证明。6结论通过扩展[3，4，5]中提出的方法，我们能够半自动地计算Futurebus+Cache Coherence Protocol的网络不变量。据我们所知，这是第一个正确的网络不变量。建立了之前未示出的新的进度属性（参见等式（5）{（7））。这导致将PAX应用于一个大型示例。使用组合推理，我们已经表明，Futurebus+ Cache Coherence Protocol的一般情况下的网络不变量与VEPAS 2001 {M.基亚斯14网络不变的协议的单总线的情况下。结果表明，计算和验证网络不变量所需的时间远远少于模型检查由两个处理器组成这使得这里提出的方法有希望应用到其他大型的例子。相关工作。Futurebus+高速缓存一致性协议的精确模型是通过E. Clarke et al. [11].他们使用时序逻辑模型检查来证明该协议满足缓存一致性的形式化规范。他们已经验证了一个选择的例子，而不是一个参数化的版本。我们基于他们的缓存一致性规范，并使用新的进度属性对其进行扩展。在[20，6]中验证了方案的参数化版本。这两项研究都只验证了[11]中给出的规范的一个子集在[20]中，网络的状态被编码为一种正则语言，其组成过程的状态的字母表和转移关系由nite状态转换器表示。这个想法在[1，7]中得到了改进，其中这种方法被称为常规模型检查。该方法已在Pen程序中实现[24]。我们的方法基于类似的想法。对于某些系统，可以用D.Lesens[23]，其中加宽技术[13]用于计算线性参数化网络的网络不变量。这个想法和我们的相似。所有这些方法都是半自动的，或者可能无法终止。我们已经使用PAX来计算Futurebus+ Cache Coherence Protocol的单总线配置的网络不变量[21，29]。这样的网络不变量在[12，22]中描述。[12]中给出的网络不变量是不正确的。虽然抽象关系是相似的，但[12]中的证明是手工完成的。我们的半自动方法增加了在既定的证据的置信度。在[16]中，证明了线性Futurebus+ Cache Coherence协议的验证问题是可判定的。然而，PAX的验证非常快。只需要两分钟就可以完成系统的验证。使用一个传统的模型检查器和2个处理器需要36个小时来检查我们的规格。引用[1] P. A. Abdulla，A.布阿贾尼湾Johnson和M.尼尔森参数化系统验证中全局条件的处理在Halbwachs和Peled [17]。[2] K. R. Apt和D. C.浩善nite-state并发系统自动验证的限制。 信息处理快报，6（22），1986年。VEPAS 2001 {M.基亚斯15[3] K.包库斯，S. Bensalem，Y. Lakhnech和K.斯塔尔抽象WS1S系统以验证参数化网络。In S. Graf和M. Schwartzbach，编辑，Proc.TACAS '00，LNCS第1785卷。斯普林格，2000年。[4] K.包库斯岛Lakhnech和K.斯塔尔参数化网络的普适性质。In M. Joseph编辑，Proc.FTRTF2000，LNCS第1926卷。斯普林格，2000年。[5] Kai Baukus，Yassine Lakhnech，and Karsten Stahl.参数化协议的验证。杂志 《通用计算机科学》，7（2），2001年。[6] S. Bensalem，Y. Lakhnech和S.嗷自动和组合地计算处于夜间状态的系统的抽象。以. J.Hu和M. Y. Vardi，编辑，Proc.CAV '98，LNCS第1427卷。Springer，1998年。[7] A. 布阿贾尼湾Jonsson，M.Nilsson和T.Touilli。定期模型检查。在大肠A.Emerson和A. P. Sistla，编辑，Proc.CAV '00，LNCS第1855卷。斯普林格，2000年。[8] J. RichardBuc 你 好 。weak 二 阶 算 术 和 nite 自 动 机 。FU杂志rmathematischeLogikundGrun dlagenderMathematik，6，1960.[9] A. Cimatti，E.克拉克角，澳-地Giunchiglia和M.罗维里NuSMV：一种新的符号模型验证器。在Halbwachs和Peled [17]。[10] E. M. Clarke和E. A.爱默生使用分支时间时序逻辑设计与综合同步骨架。InD. Kozen，编辑，程序逻辑研讨会，LNCS第131卷。Springer，1981年。[11] E. M. Clarke ， O. Grumberg ， H. Hiraishi ， S. Jha ， D. E. 朗 ， K. L.McMillan和L. A.奈斯验证Futurebus+高速缓存一致性协议。在L. Claesen，编辑，Proc. 11th Int. Symp.补偿硬件描述Lang.App.NorthHolland，1993年。[12] E. M. Clarke，O. Grumberg和D. A.佩尔德。模型检查。 MIT Press，1999.[13] R. Cousot和P. Cousot。抽象解释：一种统一的格模型，用于通过构造或近似xpoint来对程序进行静态分析。第四届ACM Symp. 关于Prog.浪，1977年。[14] W.- P. de Roever和K.恩格尔哈特数据检索：面向模型的证明方法及其比较。 剑桥大学出版社，1998年。[15] C. C.埃尔戈特nite自动机设计的决策问题及相关算法。 《美国数学学会》，98，1961年。[16] E. A. Emerson和K. S.南条参数化同步系统的自动验证。In R. Alzheimer和T. A. Henzinger，编辑，Proc.CAV '96，LNCS第1102卷。Springer，1996年。[17] N. Halbwachs 和 D. 编 辑 ， 编 辑 。 Proc. CAV '99 ， Volume 1633 ofLNCS.VEPAS 2001 {M.基亚斯16Springer，1999年。VEPAS 2001 {M.基亚斯17[18] J. G. Henriksen，J.詹森，M。J rgensen，N.克拉隆德湾佩奇，T。劳厄，A. 桑德霍尔姆Mona：Monadic second order logic in practice一元二阶逻辑在实践中在TACAS '95中，LNCS的第1019卷。Springer，1996年。[19] IEEE Futurebus+标准|逻辑协议规范，1992年。[20] Y. Kesten，O. Maler，M. Marcus，A. Pnueli和E.沙哈尔使用丰富的断言语言进行符号模型检查。号手术Grumberg，编辑，Proc.CAV '97，LNCS第1254卷。Springer，1997年。[21] R. Kurshan和K.L. 麦克米兰过程的结构归纳定理在ACM Symp. 上一篇：关于DistComp. ，1989年。[22] M. 凯亚通过提取验证Netzwerke参数。 硕士论文，Institutfu信息与实践数 学 ， 基督教- 阿 尔 布 雷大学at ， Kiel ， 2000.在 英 语 中 ， 可 以在www.example.com上http://www.informatik。uni-kiel.de/~mky/publications/。[23] D.莱森斯反应系统的验证与合成。格勒诺布尔国立综合理工 学 院 博 士论文，1997年9月。[24] M.尼尔森分析参数化分布式算法。硕士论文，系。 计算机系统，1999年。[25] A.普努埃利程序的时序逻辑。1977年，第18届IEEE计算机科学。[26] J. P. Queille和J.Sifakis cesar中并发系统的规范与验证。 InM. Dezani-Ciancaglini和M. 莫塔纳里，编辑，P roc。第五届国际Symp. 《程序设计》第137卷Springer，1981年。[27] L.斯托克梅尔自动机理论与逻辑中决策问题的复杂性。麻省理工学院电气工程系博士论文，剑桥，文学硕士，1974.[28] W. 托马斯语言、自动机和逻辑。In G.Rozenberg和A.Salomaa，编辑，《形式语言手册》，第三卷。Springer，1997年。[29] P. Wolper和V.洛文福斯具有网络不变量的大型过程集的可拓性质在J.Sifakis，编辑，Proc.CAV '89，LNCS第407卷。Springer，1989年。
我的内容管理
展开
