理论计算机科学电子笔记185（2007）93-105www.elsevier.com/locate/entcs基于有向模型检测Sara Gradara、Antonella Santone和Maria Luisa VillaniRCOST -意大利电邮地址：{gradara，santone，villani}@ unisannio.it摘要模型检查是从状态爆炸问题中产生的，这是由于随着系统组件数量的增加，有限状态模型的大小呈指数级增长。定向模型检查旨在通过基于搜索策略来减少这个问题。 在对公式进行检验的同时建立了系统的模型，模型的建立是在启发式函数的指导下进行的。 在这一行中，我们定义了一个基于结构的启发式函数，它作用于通信系统微积分（CCS）中描述的过程，它解释了要验证的公式的结构，用选择性Hennessy-Milner逻辑表示。我们已经实现了一个工具来评估该方法，并验证了一些公式的知名CCS过程的样本，报告和评论了结果保留字：模型检测，启发式搜索，CCS，逻辑。1引言模型检查[9]是一种形式化验证有限状态并发系统的方法。它源于由交错表示并发引起的著名的状态爆炸问题。毫不奇怪，模型检查中的大多数研究都集中在最大限度地减少状态爆炸的影响的方法上，例如符号模型检查[25]，on-the-dummy [23]，局部模型检查[33]，偏序[15，28]，抽象[8]和组合推理[10，29]。近年来，将模型检测和逻辑学结合起来，指导系统状态图的研究，引起了人们极大的兴趣。 对于软件验证，在Yang和Dill [34]的工作中，模型检查器的错误查找能力通过使用逻辑学来搜索最有可能导致错误的状态来增强。在[14]已经引入了定向模型检查的概念传统的模型检测算法基于深度优先或广度优先搜索算法执行不知情的状态空间探索在定向模型检查中，使用启发式搜索算法，如A* [27]，以引导搜索到最短或接近最短的路径，进入违反属性的状态。几种方法1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.05.03194S. Gradara等人/理论计算机科学电子笔记185（2007）93已经在用于显式状态模型检查的启发式搜索的领域中提出，例如参见[13，16，24]。我们的工作与那些不同之处在于，我们提供了一种使用启发式搜索来加速验证而不是发现错误的方法。在本文中，我们提出了我们对描述为通信系统（CCS）[26]过程的并发系统的验证的贡献。我们使用选择性Hennessy-Milner（SHM）[5]逻辑来表达要验证的属性。根据[32]中的分类，我们成功管理的属性 我们的方法的思想是，如果可能的话，避免生成整个系统的全局状态图进行验证。我们使用一个启发式函数来修剪状态空间，并引导状态扩展到最接近的感兴趣的状态的SHM公式在手。根据一些规则，沿着状态展开对要验证的SHM公式进行约简，并将其考虑到跃迁的生成。一旦我们可以推断出系统是否满足原始SHM公式，我们就停止状态空间如果启发式函数是一致的1，则当应用诸如A* 的搜索算法时，保证解的最优性。在本文中，我们提出了一个启发式的定义和例子，证明这种方法可以真正提高搜索相比，穷举搜索。不同准确度水平的其他（一致）启发式定义见[20]。我们的启发式函数是在语法上定义的，即， 根据CCS规范和公式的结构。此外，它们可以自动计算，因此不需要用户干预和手动操作。已经开发了一个实施我们的方法的工具，并考虑了现实生活中的基准案例研究，以供评估。2背景我们假设读者熟悉启发式搜索的基本概念，我们参考[27]了解详细信息。2.1通信系统的微积分我们简要回顾了通信系统微积分（CCS）的基本概念[26]。进程的语法是：p：：= nil|α。p|p+p|p|p|p\L|p[f]|X其中，α在有限个动作集合A ={τ，a，a，b，. }，τ称为内部作用量。可见动作的集合V被定义为A − {τ}，L<$V，重新标记函数f是一个全函数，f：A → A。给定L<$V，用L表示集合{l|l∈L}。x的范围是一组常量名：每个常量x1如果一个状态和它的后代之间的启发式估计的差异小于或等于连接它们的边上的实际路径成本，则启发式函数是一致的。S. Gradara等人/理论计算机科学电子笔记185（2007）9395法pα−→pJp−→pαJα.pα总和和sym。Par和sym。−→pp+q−→pαJp|q−→p|QαJLJαJαJ网p−→p，q −→qLJp|Qτ PJ|QJConp−→xαx−→pdefX p=p−→p−→pJXResα/∈（L<$L）p\L−→p\LαJpα−→pJRelp[f]−→p[f]f（αdef由常数x=p定义。 进程p的语义是通过图1所示的结构化操作语义来定义。语义定义描述了对应于CCS过程p的自动机的转移关系，称为p的标准转移系统，并表示为S（p）。Fig. 1. CCS的标准操作语义给定一个p，我们使用First（p）={α|p−α→pJ}不确定p可以执行的所有第一个操作的集合。它可以在语法上被定义为[26]中给出的排序的定义。给定一个过程p，p的一个常数x被称为在p被保护，如果x包含在p的一个形式为α.q的子过程中，其中q是一个过程。一个进程p是有保护的，如果p的每个常数在p中都是有保护的，否则它是无保护在下文中，展开x（p）是通过将每个未保护常数x替换为它的定义而获得的过程。对于一个实例，ifxd=efa.x，Unfoldx（（a. B. X|x）\{a}）是过程ss（a.b.x|a. x）\{a}。从现在开始，对于每个过程q=（q1|··· |q n）我们假设如果一个作用α是关于q i的s或t2，其中h i∈[1. n]和α∈[1. n]且i/= j，则过程q在限制集L下发生，使得L<$L包含α。如果α和α都出现在一个过程中，那么可以合理地假设它们是通信动作。2.2选择Hennessy-Milner逻辑选择Hennessy-Milner逻辑（SHM逻辑）是作者等人在[5]中提出的选择μ-演算的一个子逻辑，它比Hennessy-Milner逻辑更有表现力[32]。SHM逻辑的语法如下，其中K和R在动作集上变化：：：= tt|FF|ϕ∧ϕ|ϕ∨ϕ|[K] R|K过渡系统状态s对SHM公式的满足，S| = 0，是这样定义的：• 每个州满足tt，没有州满足ff;• 如果一个国家满足1.1或（和）1.2，则它满足1.1（1.2）1.2;2 CCS过程p的排序是p的字母表[26]。96S. Gradara等人/理论计算机科学电子笔记185（2007）93• [K]R满足于这样一种状态，即，对于不属于RK的一系列动作的每一次执行，接着是K中的一个动作，该状态演化为服从K的状态。• 满足于K的是一种状态，这种状态可以通过执行一系列不属于R的动作，然后是K中的动作，进化到服从K的状态。选择模态算子<$K<$R<$和[K]R<$取代了标准模态算子<$K<$$>和[K]<$。我们使用这种逻辑，因为只有选择模态算子明确提到的动作才能被启发式函数用来建议更有希望的节点。我们给出了一些SHM公式的例子来说明选择算子的使用。1=[b]{a}ff：“如果之前没有执行过动作a，则2= [a]{b}3例如，过程：p=a.b.c.nil+c.a.b.nil满足条件1和条件3，但不满足条件2。3CCS过程模型检验的一种启发式函数该方法的思想是在验证公式时避免构建整个过渡系统，而只考虑其中足以得出正确结论的部分。 为此，我们使用一个启发式函数来建议访问哪些状态，以便能够在状态空间的构造过程中尽快确定公式是否满足。在我们的启发式中，公式中出现的第一个动作表明最有希望扩展的节点给定CCS过程p和SHM公式，我们将公式验证形式化为状态空间搜索问题，作为四元组（N，O，N0，G），其中N是节点集，即元组S，S是属于转换系统S（p）的状态，S是S的子公式;O是图2中定义的一组运算符N −→ N;N0=Sp，S是初始节点;G是N的子集，称为目标节点。在下文中，我们将定义何时节点是公式的目标节点验证问题。我们在图2中非正式地解释规则。在菱形1规则中，如果p可以执行α以成为pJ，其中α∈K，即，第一个动作是α，然后是元组p，第一次行动后的剩余部分。如果α/∈K<$R，如菱形 2规则，则元组<$p，<$K<$R<$<$可以执行α以变为<$pJ，<$K<$R<$<$，其中公式没有改变。这对于框1和框2规则是相同的。值得注意的是，在菱形规则中，α∈R的情况没有被包括在内。 这是因为如果S. Gradara等人/理论计算机科学电子笔记185（2007）9397^^^^ ^您的位置：^钻石1pα−→pJp，αα∈Kdiamond2pα−→pJp，αα/∈ RK方框1pα−→pJp，[K]Rαα∈K方框2pα−→pJp，[K]Rααα/∈ RK或1p，α1p，2p，−→或21p，−→2和1p，−→1p，−→2p，α和21p，α2图二. 操作语义学的基本概念。p可以执行一个属于R的动作，该动作的跃迁不影响公式的真值α∈R的情况也没有包括在盒子规则中，因为在这种情况下p的跃迁总是满足公式[K]R。或（resp.）和）规则，对国家的法律，2011年12月2日（分别）。p，它们之间的区别在于对公式验证目标的定义例如，考虑过程p=a.nil和公式1=attbtt和2=attbtt。无论是在2011年，因此，2002年将向以下情况提供指导：−a→bn i l，ttnand−→bnil，ttnbntt。∅然而，只有p，1是一个成功的节点（参见本节末尾的测试我们首先定义了你的乐趣。定义3.1[h（np，n j）]设p是CCS过程，n是SHM公式，p和L是可见动作集，C是对{nx，L J n}的集合，其中x是p中出现的常数，L J n V，U是常数集。首先，我们用五个参数h（p，L，ρ，C，U）在p上归纳定义辅助函数h，如图3所示。 然后，h（p，p，p，p）被定义为h（p，p，p，p，p），其中p是在公式3上发生的第一个动作的集合。启发式函数h（p，L，ρ，C，U）相对于约束环境L，（L <$V）是参数化的，保持某些约束成立的动作集合。该函数最初应用于L=L的过程，当该函数应用于p\L时，L被修改（规则R5），将L中的动作添加到L中。请注意，每当计算常量x的环境发生变化时，我们都会扩展常量x的主体（规则R7）。每个已经展开的常量都与当前环境一起存储在C中。最初，C=0。集合ρ包含在验证中的公式上发生的第一个动作直觉，3更准确地说，设和J为SHM公式。发生在第一个动作中的动作集合归纳定义如下：F（tt）=F（ff）=F（KR）=F（[K]R）=KF（J）= F（J）=F（）F（J）98S. Gradara等人/理论计算机科学电子笔记185（2007）93⎧^⎧⎩⎧^h（U nf oldx（p1| · · ·|pn），L，ρ，C，U<${x}）1 +^h（p1| · · ·|Q| · · ·|R| · · ·|pn，L，ρ，C，U）h（pi，L，ρ，C，U）nR1^h（nil，L，ρ，C，U）=∞R2. h（α，p，L，ρ，C，U）=<$0，如果α∈ ρ<$L在这两种 情况下，R3.^h（p1+p2，L，ρ，C，U）=min（^h（p1，L，ρ，C，U），^h（p2，L，ρ，C，U））R4^h（p1| · · ·|pn，L，ρ，C，U）=如果 n是p 1中的无保护常数x，|··· |p n，其中x/∈ U⎪0波夫峰⎪是被保护的，i∈ [1.. n]，且n∈ [1..标准时间pi=α.q，α∈ρ ^1k n1+ h（p |Q|q|p|p⎪⎨，L，ρ，C，U）ifpisguarded，i∈[1.. n]，且ndk=min{j|pj=αj。qj，αj/∈L<$ρ}如果p i是守护的且First（p i）<$L，<$i ∈ [1. n]和你好！ α∈Ls.t. pi=α。q，pj=α. randα，α∈/First（pk）⎪∀k∈ [1.. n] k/= i/= j⎪CITD我不知道他是谁f^h（p，L，ρ，C，U）=∞，wheereD=0布Σi=1，我^h（pi，L，ρ，C，U）orwis e∞R5.^h（p\L，L，ρ，C，U）=^h（p，L<$L<$L，ρ，C，U）R6.^h（p[f]，L，ρ，C，U）=^h（p，f−1（L），f−1（ρ），C，U）R7^h（x，L，ρ，C，U）=<$∞if<$x，L<$∈Cdefn^h（p，L，ρ， C<${<$x，L<$}，U））if<$x，L<$/∈Canddx=pS. Gradara等人/理论计算机科学电子笔记185（2007）9399FIG。3.第三章。S HM的bhfunctionformular iverifiecation。h（n，n）返回在执行在n中的第一个模态运算符中发生的动作之前要执行的动作的最小数量，即，在ρ中的动作。的节点^100S. Gradara等人/理论计算机科学电子笔记185（2007）93^^能在ρ中执行操作的更有希望。 对于p=nil（规则R1），函数 h返回∞，因为nil不能执行ρ中的操作，因为它根本不能执行任何操作。当应用于α.p（规则R2）时，如果α是公式的第一个动作（即，α∈ρ）或者如果α∈ L（因为动作α可以执行，所以我们乐观地返回0），否则函数递归地应用于寻找ρ中的动作（如果有的话）。当遇到两个进程的选择时（规则R3），返回在两个组件之间执行ρ中的操作之前的最小操作现在，让我们考虑进程的并行组合（规则R4）。在这种情况下，试探法的准确性水平可以根据是否放松对它一致的要求而变化在这个定义中，我们选择了一种基于语法的方法，在不考虑所有可能的线程交织的情况下，简单地返回一个（可能不是最佳的）不属于ρ的非通信操作的数量，这些操作可以由线程执行。因此，我们首先展开平行合成中出现的未保护常数。这可以通过将展开的常数存储在U中来完成.此外，在所有并联组件都被保护的情况下，如果存在并联组合的组件可以执行公式的第一个动作，即，在ρ中执行一个动作，则返回0，因为进程可以立即执行该动作。此外，如果：• 存在平行合成的独立分量，即，可以执行不属于ρ（pi= α.q且α/∈ L <$ρ）的非限制动作的过程;或• 所有组件只能执行受限的动作，并且存在一个且只有一个进程对可以在受限动作上通信，并且这个唯一的进程对具有（α.q，α.r）的形式;那么动作的估计数量是1加上由函数的递归应用返回的值。在所有其他情况下，如果并行组合的每个进程的h值为∞，也就是说，它们中的每一个都不能在ρ中执行一个动作，所以它们的合成，因此我们返回∞;如果不是，则返回每个并行过程p i的动作数之和，而不考虑具有无限h值的过程。当考虑一个重新标号的过程时（规则R6），我们必须把集合f −1（ρ）作为第一行动的集合，把集合f −1（L）4作为限制行动的集合。最后，（规则R7），当我们遇到一个在相同环境下已经展开的常数时（更准确地说，当我们遇到一个常数x，L ∈C）。 在这种情况下，没有发现ρ的我们在R7中使用了简单的示例。 C〇nsiderxd=efa. y和dyd=efb。X.假设我们想验证x是否满足=ct。我们将定义应用于f^h ，其中 hρ={c}。Therefor：^h（x，n，p，n，n）=^h（a. y，n，ρ，{nx，nn}，n）（byRuleR7，nx，nn n/∈C）4给定一组动作S，f −1（S）={α |f（α）∈ S}.^S. Gradara等人/理论计算机科学电子笔记185（2007）93101^^^^^^ ^您的位置：=h（y，n，p，{nx，n n}，n）（根据规则R2）= ∞（根据规则R7，x，x ∈ C）。值∞意味着进程x不能执行动作c。我们现在可以用R4.Considerxd=efa.x，yd=efa.k1，zd=efa.k2anddwd=efd. W.假设我们想验证p =（x|y|z|w）\{a}满足=c。我们可以定义为^hw i thp={c}。Therefor：h（p，n，p，n，n）= h（x|y|z|w，{a，a}，ρ，ε，ε）（根据规则R5）= h（a.x|a.k1|a.k2|d.w，{a，a}，ρ，ρ，{x，y，z，w}）（通过规则R4分支1四次）= 0（根据规则R4分支5）。注意h（d.w，{a，a}，ρ，ρ，{x，y，z，w}）= ∞一旦定义了启发式函数，我们就可以应用搜索策略。搜索策略扩展节点，直到它可以推断出开始节点是成功节点还是不成功节点，基于以下应用于节点n的函数测试，如果n是成功节点，则返回s，如果n是不成功节点，则返回u• test（intp，int t）=s;• test（p，12）=s iftest（p，1）=stest（p，2）=s;• test（p，12）=s iftest（p，1）=stest（p，2）=s;• test（np，[K]Rnp）=s如果h（np，[K]Rnp）=∞或test（m）=snm∈{nJ|n−α→nJ，α/∈R};• t est（np，nK<$R<$p）=sif<$m∈{nJ|n−α→nJ，α/∈R}满足tt est（m）=s.• return（p，ff）;• test（p，12）=u iftest（p，1）=utest（p，2）=u;• test（p，12）=u iftest（p，1）=utest（p，2）=u;• test（p，<$K<$R<$$>）=u如果h（p，<$K<$R<$$>））=∞或test（m）=u<$m∈{nJ|n−α→nJ，α/∈R};• t est（np，[K]Rnn）=uifnm∈{nJ|n−α→nJ，α/∈R}满足tt est（m）=u.现在考虑简单的CCS过程p=a.b.g.x+a.d.b.x+b. d. b.c. nil;其中xd=efb.d.nil. 针对11个数据的传输位置系统。请使用两种方法验证以下SHM公式：d=ef[a]它认为p是满足的。我们注意到，对于p，只访问7个节点就足以说明公式对于过程p是满足的，而p的标准转移系统有11个状态。让我们将我们的方法应用于具有贪婪搜索策略的过程p。当选择足够多的节点以基于功能测试的定义推断起始节点是成功节点还是不成功节点时，节点扩展终止。102S. Gradara等人/理论计算机科学电子笔记185（2007）93在图4中，记录了一个节点的h-v值。因为，我认为这是S. Gradara等人/理论计算机科学电子笔记185（2007）93103
一一BBTT> S2，b>BTT>S4，b> BTT> S5，b S6，b> BTT>BD^h=Btt>^h=10b一一BBTT> S2，b>BTT>S4，b> BTT> S5，b S6，b> BTT>^h=0^h=2^h=^h=(a)（b）第（1）款FIG。 四、 这是一个简单的例子。h（S15，bt）= 0意味着进程S1可以立即执行相应公式的第一个动作，即b。应用Greedy搜索策略，首先我们扩展节点P2p，P2p：生成三个状态：P2p1，P2p2，P2p2，P2p3，P2p3（见图4（a））。在图4（a）和图4（b）中，阴影节点表示要扩展的状态。然后，我们选择首先展开具有最小h值（等于0）的S1，btt，生成S4，tt，然后展开h值等于1的S2，btt最后，我们展开S5，btt，h值等于0，生成S6，tt（见图4（b））。基于成功/不成功节点的定义，由于过程4，ttn，过程6，ttn和过程3，ttn是成功节点，我们可以停止过渡系统的构造，说明过程p满足公式n。4实验结果所提出的方法已在一个工具中实现，该工具是DELFIN+（DEadloack FINder）的扩展[18，19]。事实上，该工具的前一个版本专门用于死锁检测，提供了一组可与A*、IDA* 和Greedy等明智的搜索策略一起使用的算法。增加的功能包括通过应用第3节中提出的基于公式的启发式，针对选择性Hennessy-Milner逻辑中表达的任何类型的公式来验证CCS过程的可能性。我们在Intel Pentium 4上运行了一些实验，处理器为2.80 GHz，内存为1 GB，总体上可以观察到令人鼓舞的结果。我们从文献中选择了一个众所周知的系统和一些有趣的性质来验证，这些性质在下面描述。用于移动计算的多播协议（MPMC）：在[2，3]中提出的用于分布式移动系统中的可靠多播的协议。在此系统上，我们检查了以下两个SHM公式：1=[deliver（m，msg）]{send（msg）}ff5S1= b.g.x.^104S. Gradara等人/理论计算机科学电子笔记185（2007）93表示由组成员递送的任何多播已经由组成员发起的属性;以及2=[deliver（m，msg）]表示没有组成员传递重复的多播，即，丢弃重复的多播。这两个性质都是真实的，并且由新世纪的并发计算器（CWB-NC）[11]构造的标记转移系统的大小由4， 815个状态组成。使用我们的工具，在生成146个状态后验证了属性141，而对于属性142，没有得到任何减少。GRID：在一个5× 5的中继站网格上的两个进程，允许它们进行通信。这个例子取自[6]。在这个系统上，我们考虑了平凡的SHM公式，表示存在连接两个过程的路径的性质。<财产是满意的。CWB-NC未能验证该过程中的任何公式，因为其标记的转换系统太大而无法加载。使用我们的工具，我们用两个初始分别位于（1，1）和（5，5）的过程验证了公式，在生成11，509个状态后给出了真实结果MUTUAL：一个系统处理10个进程共享的资源请求。它提出了两种替代选择之间的服务器基于轮询调度和服务器的基础上互斥。在此系统上，我们检查了以下两个SHM公式1= [roundrobin]2=[worki+1]{worki}ffR1表示当选择基于循环调度的服务器时，进程i + 1不能使用进程i之前的资源的属性。 这个属性是满足的，相反，系统不满足表示一般来说，进程i+1不能在进程i之前使用资源的属性。CWB-NC构建了一个由32， 768个状态组成的系统，而使用我们的工具，i= 1，我们在生成13， 824个状态后成功验证了公式1，在生成89个状态后成功验证了公式2Philips有限重传协议（BRP）：Philips公司在其产品中使用的有限重传协议[17，21，22]。在此系统上，我们检查了以下两个SHM公式：1=[in（d1di）]2=[in（d1di）]公式1表示，在接受长度为i的数据包后，协议不能向发送客户端发出ok确认（actionin（ok）），除非数据包的最后一段（actionout（di，ok））已经被发送到接收客户端。公式nok2意味着，在接受长度为i的数据包后，协议可以向发送客户端发出nok确认（actionin（nok））。这两个属性都很满意。由CWB-NCS. Gradara等人/理论计算机科学电子笔记185（2007）93105是759个状态，而使用我们的工具，i= 3，我们可以在558 个状态后验证101，在34个状态后验证102固态联锁（SSI）：英国铁路公司该系统致力于“根据信号操作员的要求，调整铁路上的信号和点的设置，以允许列车安全通过”。在此系统上，我们检查了以下SHM公式：[det]{fail} ff。 该公式意味着，只有当已经发生了 该系统不满足1991年。 在这个过程中，CWB-NC构造了一个3616个状态的标号跃迁系统，而我们的工具可以在生成361个状态后验证公式是假的接龙游戏（SG）：一个CCS规格的接龙游戏[4]，由卢卡Aceto开发（可在[1]）。该系统满足以下SHM公式：1=w 1，w 2，w 3，b 5，b 6，b 7tt。CWB-NC的这个过程的标记转换系统由3， 107个状态组成，但我们的工具使用431个状态来验证。除了这些过程，为了更好地评估我们的启发式，我们考虑了哲学家用餐过程的僵局版本，并检查了一个特定哲学家吃饭的可能性。我们在该过程的几个实例中这样做，即，增加哲学家的数量。所有运行的结果报告在表1中：n是哲学家的数量，数字表示在相应的运行中验证公式的生成状态的数量，通过我们的贪婪搜索工具和CWB-NC。n57911131520.30贪婪177440816 1389 2055 2847 5387 . 12867CWB-NC 2404 54142 −−−−−−−表1关于用餐哲学家从表中可以看出，CWB-NC无法从n= 9开始加载过程，而使用我们的工具，我们甚至可以对30位哲学家的配置进行模型检查。5相关工作和结论在本文中，我们提出了一种方法和工具，适用于并发系统描述为CCS进程的有向模型检测。要验证的性质（弱活性和安全性）在选择性Hennessy-Milner逻辑[5]中表示，这是一种分支时间逻辑。所提出的方法的效率显示在一些例子中，众所周知的文献中，贪婪策略已被应用在一起的启发式图3。与此最密切相关的工作在[12]中提出，其中作者提出了一种基于待验证的LTL（线性时序逻辑）属性然而，他们的工作集中在活性特性上，106S. Gradara等人/理论计算机科学电子笔记185（2007）93以及不变式和断言错误。[12]中的方法进一步用[31]中的贝叶斯推理进行了改进，其中重点不是对统计学的研究和定义，而是应用统计方法来提高引导搜索的预期精度。这是通过将启发式估计解释为随机变量而不是点值来获得的。在[13]中，Hamming距离启发式被用来指导SPIN中的错误搜索。这种技术要求首先识别出发生错误的系统的特定状态;然后使用该状态与当前系统状态之间的汉明对于达到给定违反状态的简短反例。在[24]中，逻辑学已被应用于通信协议的验证。考虑了无死锁等安全特性在一篇先驱论文[30]中，其中一位作者将AO* [27]与局部模型检查相结合，以验证CCS过程。这是第一次通过直接模型检查进行验证，提供了启发式函数的示例。 作为该工作的扩展，我们提出了另一个启发式函数定义，可以很容易地定制死锁检测。事实上，在[19]中，作者提出了死锁特异性算法，并通过DELFIN+在几个示例上分析了它们的效率。因此，一旦定义了启发式函数，并且基于公式，就可以使用几种启发式搜索策略（Greedy、A*、IDA*、AO*等）。最后，其他众所周知的约简技术，如偏序，组合推理，抽象，可以作为局部模型检查的替代。作为未来的工作，我们打算着手分析更准确的启发式函数，并加深对其他案例研究的方法的评价。我们有兴趣将这种方法与抽象技术相结合，以实现进一步的改进。引用[1] L.Aceto.的接龙。http://www.cs.auc.dk/www.example.com[2] G. Anastasi，A. Bartoli，N.德·弗朗西斯科。移动计算多播协议的有效验证。计算机杂志，44（1），（2001）。21-30[3] G. Anastasi ， F. Spadoni， A.巴 托 丽 不 可 靠 无 线 网 络 下 分 布 式 移 动 系 统 中 的 组 多 播 。 在 SRDS '99：Proceedings of the 18th IEEE Symposium on Reliable Distributed Systems. IEEE Computer Society ，14，（1999）. 14比23[4] A. Arnold，D.贝盖，P.克鲁比尔。用MEC构造和分析变迁系统。《世界科学》，第6章，1994年。[5] R. Barbuti，N. De Francesco，A. Santone，G.瓦格里尼转换系统的选择性μ演算和基于公式的抽象。Journal of Computer and System Sciences，59（3），1999，537-556.[6] J. Brad Field，C.斯特灵进程的时间属性。CONCUR '90：Theories of Concurrency - Uni fication andExtension（1990）Springer，1990年。115-125.[7] G.布伦斯安全关键设计案例研究。CAV'92：计算机辅助验证第四届国际研讨会论文集Springer，1992年220-233.[8] E.M. Clarke，O. Grumberg，D.E.久了模型检查和抽象。ACM Transactions on Programming Languagesand Systems，16（5），1994。1512-1542年。[9] E.M. Clarke，O. Grumberg，D.佩尔德。模型检查。 麻省理工学院出版社，2000年。S. Gradara等人/理论计算机科学电子笔记185（2007）93107[10] E.M. Clarke，D. E. Long，K.L.麦克米兰组合模型检查。在第四届IEEE计算机科学逻辑年会上，1989年。353-362.[11]R. Cleaveland，S.西姆斯NCSU Concurrency在第八届计算机辅助验证国际会议（CAV'96）的会议记录394-397.[12] S. Edelkamp，A. Lluch-Lafuente，S. Leue使用HSF-SPIN进行有向显式模型检查。第八届国际SPIN模型检测软件研讨会论文集，计算机科学讲义2057，2001。57比79[13] S. Edelkamp ， A. Lluch-Lafuente ， S. Leue Trail-directed model checking. 电 子 笔 记 理 论 计 算 机 科 学（ENTCS）55，2001年。[14] S. Edelkamp，A. Lluch-Lafuente，S. Leue通信协议验证中的有向显式状态模型检验。国际软件工具技术转移杂志，2004年6月。257-259.[15] P. Godefroid。并发系统验证的偏序方法。LNCS 1032，1996年。[16] P. Godefroid，S.胡尔希德用遗传算法探索超大型状态空间。在第八届国际会议的工具和算法的建设和分析系统（TACAS266-280。[17] J. F. Groote，J. van de Pol.A Bounded Retransmission Protocol for Large Data Packets.数学方法与软件技术，1996。536-550.[18] S. Gradara，A.题名其余部分：M.使用启发式搜索发现并发系统中的死锁。信息与计算，202（2），2005。191-226[19] S. Gradara，A.题名其余部分：M.DELFIN+：一个高效的CCS进程死锁检测工具。发表在Journal ofComputer and System Sciences上。[20] S. Gradara，A.题名其余部分：M. 定向模型检查CCS进程。技术报告，TR-RCOST 12/03，2006年2月。[21] K. Havelund，N.史恩卡协议验证的定理证明和模型检测实验。FME'96：Industrial Benefit and Advancesin Formal Methods，Springer-Verlag，1996年662-681.[22] L. Helmink，M. P. A. Sellink，F. W. 凡德拉格 验证-检查数据链路协议。 在TYPES127比165[23] C. Jard，T. J'eron. 有界内存Algorithm s forVerification-the-socket. 在第三届计算机辅助验证国际会议（CAV'91）的主持 人，LNCS 575 ，1991。192-201.[24] F.J. Lin，P.M.Chu，M.T.刘某使用可达性分析的协议验证：状态空间爆炸问题和缓解策略。ACM，1988年。126-135.[25] K.麦克米兰 符号模型检查。 Boston：Kluwer Academic Publishers，1993.[26] R.米尔纳 通信和并发。 普伦蒂斯-霍尔，1989年。[27] J·珀尔启发式：计算机问题解决的智能搜索策略。艾迪森-韦斯利[28] D.佩尔德。All from One，One for All，on Model Checking Using Representatives. 第五届计算机辅助验证国际会议（CAV'93），LNCS 679，1993年409-423[29] A. Santone，使用基于公式的组合方法的并发系统自动验证，Acta Informatica，38（2），2002，531-564。[30] A. Santone 启发式搜索+局部模型检查在选择μ演算。IEEE软件工程学报，29（6），2003年。510-523[31] K.S. 塞皮M. 琼斯，P·兰伯恩 指导 模型检测 与 贝叶斯超启发式算法Fundamenta Informatica，待出版，2005年。[32] C.斯特灵CCS的模态和时态逻辑导论。并发：理论，语言和架构，计算机科学讲义391，1989。[33] C. 斯特灵，D。沃克模态Mu演算中的局部模型检测TCS，89，1991年。161-177。[34] C.H. Yang，D.L.迪尔验证与状态空间的引导搜索。第35届设计自动化会议（DAC'98），1998年599-604
