基于CLP的参数化并发系统符号验证框架

65网址：http://www.elsevier.nl/locate/entcs/volume76.html18页基于CLP的参数化并发系统符号验证框架MSR（CG. Delzannoa;1aDipartimento di Informatica e Scienze dell16146热那亚，意大利摘要在最近的工作中，我们已经定义了一个通用的框架，验证参数化并发系统的基础上组合的多集重写和约束。我们感兴趣的这类系统是由参数化的并发系统组成的。我们的框架提供了以下特点：（1）一个规格说明语言的类的并发系统的考虑;（2）断言语言来表示-sent-sent无限集的配置;（3）一个声音和全自动验证方法的基础上，符号状态探索。验证过程已在约束逻辑程序设计系统中实现，即Sicstus Prolog和CLP（Q，R）库。CLP实际上提供了所有必要的操作来操作多重集和约束，既可以作为未解释的对象，也可以作为解释的对象。对约束的操作实际上被委托给clp（Q，R）库，并封装到Sicstus Prolog谓词中。该方法可以应用于解决通信协议的验证问题，（潜在的）安全和认证协议和并发程序的抽象。在本文中，我们概述了我们的框架的主要功能，并评论一些更有趣的应用程序。1介绍在本文中，我们描述了一个通用的框架，自动验证并发系统参数的个别组件的数量我们的框架扩展了一阶原子公式（MSR）的多集重写，1电子邮件：giorgio@disi.unige.it在CC BY-NC-ND许可下开放访问。66[11]中提出的约束逻辑程序设计方法，并引入了约束逻辑程序设计[22]中特有的约束概念。虽然多集重写允许以自然的方式指定并发进程，但约束可以用于声明性地表示其内部数据之间的关系。多重集和约束的组合对于定义符号数据结构来表示系统配置的无限集合也很重要多集重写与并发的关系可以用Petri网的推理来说明。Petri网实际上可以看作是定义在有限字母表上的多集重写系统. 图中的符号表示Petri网的库所集合。一个Petri网标记可以被建模为一个多集合的符号从p：k次出现的符号p在多集合对应于k个令牌在地方p。因此，Petri网变迁可以被建模为Petri网中符号上的多集重写规则. 最后，重写步骤的序列可以被视为由相应的Petri网的执行生成的标记的序列一阶原子公式上的多集重写（MSR）[11]自然地将这种联系扩展到带有着色标记的Petri网，颜色是附加到表示标记的原子公式的一阶项重要的是要注意，在这种设置中，重写仅限于原子公式的多集直观地说，原子公式的多集合被解释为活动的和并发执行的进程的池原子公式表示各个进程的当前状态在[14，8]中，我们提出了MSR形式主义的一个推广，其中多集重写规则（一阶原子公式）被注释了约束。由此产生的语言模式，称为MSR（C），是约束系统C的参数。MSR（C）提供了过程结构和数据关系声明之间的清晰分离。这种概念分离是产生的规范的主要模块化通过组合多集和约束获得的逻辑可以自然地用于推理系统属性。具体地说，几个正确性的性质，领带可以通过搜索错误跟踪以下所谓的向后可达性搜索方案进行验证。这里的想法是首先隔离代表可能违规的配置集如果初始状态不满足这些先决条件中的任何一个，则违反永远不会发生，从而证明系统是正确的。一类特别令人感兴趣的安全特性是其违反可以通过向上闭合的配置集来表示的安全特性，即，可以通过最小的违规来表示。我们的符号表示的向上封闭集的配置是基于概念的约束配置介绍，[14]以处理异步系统，即多组一阶原子公式，注释约束。多集表示对网络中令牌分布的最小要求，而约束为不同过程的数据关系提供了自然的符号表示基于这种丰富的断言语言，我们提供了67符号操作实现向后可达性，即我们定义了一个符号前导操作，这是健全的和完整的任何约束系统。这种方法的兴趣是，允许研究不依赖于计算过程中产生的过程的数量的属性我们将澄清这一点，在本次调查中讨论的应用程序的互斥协议设计的客户端-服务器系统中，客户端的数量是没有限制的先验。我们已经实现了我们的自动化验证方法，并将其应用于分析几个实际的案例研究。一般来说，该方法在没有终止保证的情况下工作然而，一些技术，如静态分析和抽象解释可以应用于强制终止特定的案例研究。此外，可靠性确保错误跟踪最终会被发现：我们用来实现该方法的原型执行状态空间的宽度优先符号向后探索。终止只能在MSR（C）规范的特殊子类中显示[15]。作为实现平台，我们使用了一个约束逻辑程序设计系统，即CLP（Q，R）库的Sicstus Prolog。CLP提供了内置的操作和数据结构来实现基于多集的操作（统一、有效的列表表示和操作）。此外，它允许将约束处理为解释和未解释的对象。当被查询时，clp（Q，R）求解器提供了可满足性、蕴涵和投影等操作，这些操作（通过Sictus Prolog特有的封装谓词）可以嵌入到用于符号向后搜索的proc中。在本文中，我们将给出一个概述的一般框架，相应的验证方法。最后，我们将讨论CLP实现和框架的一些实际应用的问题。2约束多集重写称为MSR的框架基于定义在一阶原子公式上的多集重写系统，并且它已经由Cervesato等人引入。[11]用于加密协议的形式化规范。在[14]中，基本形式主义（即，没有存在量化）已经扩展到允许使用约束对数据变量上的关系进行指定，即在固定域上解释的逻辑语言。多集重写规则允许局部地对进程的行为和内部行为进行建模，而约束则象征性地表示不同进程的数据之间的关系，从而实现了进程结构和数据路径的清晰分离。这种形式主义可以被看作是一个一阶扩展的Petri网，其中令牌携带结构化数据。我们将所得到的形式主义称为MSR（C）。首先，我们介绍了约束系统的概念。682.1约束系统约束系统是元组C= hV;L;D;S;vc i，其中：(i) V是可数的变量集(ii) L是一种一阶语言（断言语言），它定义了一组在V（约束）中具有自由变量的公式，关于变量重命名，存在量化和合取是封闭的，并允许变量之间的等式(iii) D是一个可能的无限集合（解释域）;(iv) S（）是一组映射V！ D（约束条件的解集），它保留了等式的通常语义，^和9（解的交集和投影）;(v) v c是一个关系，使得v c蕴涵S（）S（）（蕴涵关系：我们说蕴涵）。我们假设L包含约束，表示为通过与约束规划类比，可以对约束系统提出进一步的要求，如解紧性[22]。我们参考[22]进行讨论。在本文的其余部分，我们通常用一个简单的逗号表示约束之间的连接。我们引用一个通用的映射：V！ D作为V中变量的评价。 我们用hx17来表示！d1; x27！d2;：：i表示评价将x1映射到d1，将x2映射到d2，以此类推，以及用符号jx表示求值$j对变量x的限制。我们还说，如果S（）6，则约束是可满足的。例2.1线性整数约束类由以下语法：：=其中ai2Z，对于i：1;：：;n + 1。LC-约束被解释为Z;VC是线性整数约束的通常蕴涵关系请注意，存在几种方法用于检查线性算术约束的可满足性，蕴涵和变量消除（参见[10]）。例2.2设x> y ^x> z，则= hx 7！ 2; y 7！ 1; z 7！ 0;：：：i2 S（）.此外，是可满足的，（x>y）vcn，和9y：（x>z）。我们现在准备定义带约束的多集重写的框架。69;;2.2MSR（C）语言下面我们将使用多集的概念 我们使用和来表示多集并和多集差。设P是谓词符号的有限集合，V是变量的可数集合. P和V上的原子式有形式p（x1;：：;xn）（n为0），其中p2P和x1;：：;xn是V中不同的变量。现在，设P是谓词符号的有限集合，V是变量的可数集合原子公式A1，...，A k（其中k 1）在P和V上，表示为A1j：：：j A k，其中A i和A j必须有不同的变量，i 6= j，j是结合和交换构造函数。空的多重集用表示。在本文的其余部分将使用M，N，：来表示原子公式的多集C设P是谓词符号的有限集合，C= hV;L;D;Sv i是约束系统P和C上的MSR（C）规则具有形式M！ M0：M，其中M和M0是P和V上原子公式的两个多集，具有不同的变量，且 2L.注意M！ 你好！ M：这是可能的MSR（C）规则。为了使前面的规范的直观语义精确，我们介绍了MSR规则的操作阅读的成分我们首先定义基本公式的概念。设P是谓词符号的有限集合，并且CC= hV; L; D; S v是一个约束系统。P上的基原子公式并且C具有形式p（d1;：：;dn）（其中n为0），其中p2P并且d1;：：;dn2D。在下文中，我们将用（M）表示解的应用：D到原子公式M的多重集合。形式上，如果对于xi2V和vi2D，i：1;：; m，则<$（A 1 j：j A k）$（A1）j：j $（A k），并且$（p（x1;：：;xm））=p（d1;：; d m）。给定MSR（C）规则R = M！ M0：在P和C上，R的基实例的集合，表示为Inst（R），是基多集重写规则的集合，定义如下：Inst（R）=f（M）！ （M0）j 2 S（ ）g我们语义的一个中心概念是下面给出的当前配置设P是谓词符号的有限集合，C是约束系统.MSR（C）组态是P和C上的基原子公式的多重集。可以按如下方式对多集包含进行排序给定两个原子公式的多集M4N当且仅当对每个原子公式A都有OccA（M）OccA（N），其中OccA（M）表示A在M中出现的次数.MSR（C）规范定义如下。定义2.3[MSR（C）规范]MSR（C）规范是元组hP ;C;I;Ri，其中70P是谓词符号的有限集合，C是一个约束系统，I是一组配置（初始配置），R是P和C上的MSR（C）规则集。MSR（C）规范hP;C;I;Ri的操作语义可以定义如下。设M是一个构形。规则H！B：在M处，通过约束条件的解S（），使能来自R的k，当且仅当（H）4M.现在，假设RH！B：在M处通过2S（）启用。在M上执行这个规则得到新的构型M0，记为M）RM0，当且仅当M=（H）Q，且M0=（B）Q。运行是一系列配置M0M1M2：M i：，其中M02 I，并且存在R0R1： 2R使得Mi）RiMi+1，i0.设S是一组构形.后继运算符Post定义为Post（S） =fM0jM）RM0; M2S; R2R g;而前趋算子Pre被定义为：Pre（S） =fMjM）RM0; M02S; R2Rg：precedent和successor运算符的自反闭包和传递闭包分别表示为Pre和Post可达集被定义为Post（I），I是所考虑的MSR（C）规范的初始状态。2.3标签：Ticket Mutual Exclusion Protocol票据协议是一种互斥协议，设计用于在共享内存上运行的该协议基于先进先服务的访问策略。算法如图1所示（其中我们使用P jQ表示P和Q的交错并行执行，h i表示代码的原子片段）。该协议的工作原理如下。最初，所有客户端都在思考，而t和s存储相同的初始值。当请求访问临界区时，客户端将当前票证t的值存储在其局部变量a中。然后通过递增t来发出新的票证。客户端等待轮到它们，直到它们的局部变量a的值等于s的值。在临界区内的细化之后，一个过程释放它，当前回合通过递增s来更新。在执行期间，协议的全局状态由s、t的当前值和n个进程的局部变量的当前值组成。如[10]所述，即使n =2（只有2个客户端），各个进程的局部变量以及s和t的值也可能是无界的。这意味着图1的方案的任何实例1产生无限状态71n进程系统程序全局变量：integ er;开始return0;第i分量过程Pi：：=public vara：integer;永远重复2认为： int a：=t;6return0;t：=t+1;i6P6等待：当h a=s我做1j：j Pn;结束：646用途：结束语：2临界截面4h s：=s+1;iFig. 1. Ticket Protocol：n是协议的一个参数。系统该算法应该适用于任何n值，如果新客户端在运行时进入系统，它也应该工作。多集重写使我们能够给出一个准确和灵活的编码票据协议。让我们首先考虑一个通过计数器t和s控制的单个共享资源，如2.3节所述。容许初态的无限集合是由具有任意但有限数目的思维过程和两个具有相同初始值（t = s）的计数器的所有构形规格如图所示二、初始配置是同品种器械init，即所有可能的协议运行的种子计数器在这里通过原子计数（t）和圈数（s）表示。思考客户端通过命题符号think来表示，并且可以通过第二条规则动态生成。经由图2的规则的第三块来描述单个客户端的行为，其中局部变量与全局计数器之间的关系经由DC约束来表示。最后，我们允许思维过程按照图2中最后一条规则的规定终止其执行。以前的规则与系统中当前的客户端数量无关。请注意，在我们的规范中，我们保留了数据变量的显式表示;此外，我们没有对它们的值进行任何限制因此，在我们的模型中，s和t的增长没有任何约束，就像原始协议一样。一个有两个客户端的系统的示例运行（如[10]）如图所示。3.第三章。现在让我们考虑一个开放系统，它具有任意但有限数量的共享资源，每个共享资源由两个本地计数器s和t控制。我们通过将唯一标识符与每个资源相关联来指定此外，我们利用非确定性，以模拟每个客户端选择使用哪些资源的能力。结果规范如图4所示。我们已经考虑了一个开放系统，其中新的客户端可以通过一个恶魔进程动态生成进程demon（n）维护一个本地计数器n，用于生成一个新的标识符，比如id，并将其与一个新创建的资源相关联，该资源通过对count（id;t）表示，72初始状态init！count（ t） j turn（ s）：t= s动态生成！think：真的个体行为thinkjcou nt（t） ！ wa it（a）jcou nt（t0）：a=t^t0 =t+1（a）（b）（c）（d）（e）（f）（e ！ 使用jtu r n（s0）：a=s^s0=susejtur n（s） ！ thinkjtu r n（s0）：s0=s+1终止认为！：true图二.票证协议，适用于多客户端，单服务器系统，用实例运行。init）：）think j count（8）j turn（ 8））think jthink j count（ 8）j turn（ 8））等待（8）j认为j计数（ 9）j转弯（ 8））等待（ 8）j等待（ 9）j计数（ 10）j转弯（ 8））使用j等待（9）j计数（ 10）j转弯（ 8）使用j等待（ 9）j计数（ 10）j转弯（ 8）j认为）认为j等待（9）j计数（ 10）j转（ 9）j认为图三.跑步的例子tu rn（i d;s）. 一个思考过程通过与系统中的一个计数器同步来非确定性地选择等待哪个资源（图3中第三块的第一条规则）。4）. 在此选择之后，算法的行为与通常的w.r.t.选择资源ID。终止规则可以指定为单服务器情况的自然请注意，在本说明书中，无限性的来源是客户端的数量、共享资源的数量、资源标识符的值和票证的值运行的一个例子如图所示五、3一种用于MSR的断言语言（C）由于我们可以很容易地将两个计数器机器的形式化编码为MSR（C），在MSR（C）规范中，可达性问题一般是不可判定的。即使对于MSR（C）的不具有图灵能力的片段，MSR（C）规范的可达性集也可能是无限的，因此探索它可能是极其困难的。无限性的来源可能是73生成的配置的大小（元素的数量）的增加，或者附加到原子公式的值的无界性（例如，考虑在每个规则应用时递增的简单计数器），或者两者兼而有之。74的情况。的情况。;;;;;;;初始状态init！demon（n）：true动态进程和服务器生成快！想一想：truedemo n（n）！demon（n0）jcount（idt）jturn（id0（s）：n0=n+1^t=s^id=n^id0 =id个体行为我不认为我可以！think（r）jcount（id0 t0）：r=id^i d0 =id^t0 =t t hin k（r）jcou nt（idt）！华一泰（r0 a）jcou nt（i d0 t0）：r=id^a=t^t0 =t+1^r0=r^id0 =id我是你的朋友！使用（r0 a0）jtu rn（i d0 s0）：r=id^a=s^a0 =a^s0=s^r0=r^id0 =id用户e（ra）jtu rn（ids）！tthinkjturn（id0 s0）：r=id^s0=s+1^i d0=id;;;终止think（r）！上一篇：TrueThink！：true见图4。用于多服务器、多客户端系统的票证协议。在it）demon（3））count（ 3; 0）jturn（ 3; 0）jdemon（ 4））：**）count（3;0）jturn（3;0）jthinkjthinkjdemon（4））count（3; 0）jturn（ 3; 0）jcount（ 4; 8）jturn（ 4; 8）jthinkjthinkjdemon（ 5））：）count（3; 0）jturn（ 3; 0）jcount（ 4; 8）jturn（ 4; 8）jthink（ 4）jthink（ 3）jdemon（ 5））count（3; 0）jturn（ 3; 0）jcount（ 4; 9）jturn（ 4; 8）jwait（ 4; 8）jthink（ 3）jdemon（ 5）：图五.跑步的例子自动分析这种无限状态规范的行为的唯一可能性包括找到配置的无限集合的适当的有限的符号表示。为了实现这个目标，在本节中，我们将介绍一种基于向上闭配置集概念的断言语言为了解释这个概念，让我们再次考虑例子1。假设我们有兴趣证明前几节讨论的例子的规范满足以下不变量：所有可达状态满足互斥性质，每次只有一个进程处于状态使用中。我们不直接证明它，而是可以尝试如下反75证：我们首先选择所有可能违反它的配置，然后证明它们从初始状态init不可达。的76一组有趣的违反U由像use（v）j use（w）U0这样的配置组成，其中U0是任何可能的多重集。然后，我们注意到U可以从配置M=fuse（v）juse（w）v0;w0g的（无限）集合生成，通过取关于多集包含的向上闭包：如果配置包含M的任何基实例，则它违反了自身的不变量。如[1]中所讨论的，不变性质的否定通常享有关于在配置集合上定义的包含序向上闭合的特性作为探索无限状态空间的问题的第一近似，我们可以从不安全状态开始探索，使用最小违规来表示它们，并通过应用前导算子Pre（即，计算最弱的先决条件）。让我们正式定义向上闭集的概念。设hP;C;I;Ri是MSR（C）规范，S是配置集. 的S的向上闭包，记作Up（S），定义为：上（S） =fNjM4N;M2Sg：我们说S是上闭的，如果S = Up（S）。上闭集的配置有有趣的性质，就前任运营商前。提案3.1（[15]）U p（Pre（S））Pre（U p（S））对于任何配置集合S。一般来说，相反的含义并不成立。例3.2考虑p！q1j q2和由多重集q1组成的单点集S。然后，Pre（S）=，而多重集p属于Pre（U p（S））。但是，以下属性仍然有效。推论3.3（[15]）如果S是上闭的，则Up（Pre（S））= Pre（Up（S））。换句话说，在原像的计算下，向上闭的配置集类是封闭的前面的属性不足以表示和操纵向上闭合的配置集。事实上，我们仍然要解决的问题，即我们所说的最低限度的侵犯。这并不总是可能的。然而，在单服务器票证算法的示例中，它们具有规则的结构，我们可以通过翻译扩展描述来利用该规则结构M=fuse（v）juse（w）v0;w0 g在下面的内涵描述中，称为约束配置use（x）j use（y）：true其中x;y是自由变量。 在其他方面，通过注释非接地配置（即，其中公式具有自由变量），我们可以隐式地77;表示我们对示例感兴趣的所有不安全配置。它们将对应于上述约束构型的一组地面实例的向上闭合。值得注意的是，这种技术只是一种算法，我们试图将尽可能多的配置嵌入到规则结构中在下面的部分中，我们将形式化这些想法，并展示如何将它们与[1]中提出的向后可达性方法结合3.1基于约束条件的符号表示为了表示一个向上闭的构形集的生成元，我们使用了一种基于约束构形概念的丰富断言语言，即.用约束注释的（非基础）原子公式的多集C设hP ;C;I;Ri是一个MSR（C）规范，其中C=hV;L;D;Svi. 一约束配置是P和C上的原子公式的多集，用约束标注，具有以下形式p1（x11 ;：;x1k1）j： jpn（xn1：;xnkn）：其中p1;：;pn2P，2L是可满足的约束，x1 1;：;xn kn是V中的不同变量.受约束配置的地面实例集可以定义如下。设hP ;C; I;Ri是MSR（C）规范，M：i是约束配置. M：M的基实例集定义为：Inst（M：） =f（M）2S（）g：例如，假设C是约束配置use（x）j user（y）：true。然后，如果在非负整数上解释LC约束，则Inst（C）包含像use（1）j use（ 2）、use（4）j use（ 6）等的配置。前面的定义可以扩展到约束配置的集合（de-constrained configuration）。记为S;S0）以自然方式：;：Inst（S）=[C2S仪器（C）根据我们在前一节中解释的直觉，我们选择下面的丰富表示，而不是将实例集作为约束配置集S的平坦表示设hP ;C;I;Ri是一个MSR（C）规范，S是一组约束配置（变量互不相同）.S的丰富表示，记为[[S]]，由其基实例的集合的向上闭包给出，即。[[S]]=向上（Inst（S））78的情况。例3.4设C定义为use（x）j user（y）：true。然后，[[C]]包含像use（1）juse（ 2）以及use（1）j use（ 2）j use（ 0）等这样的配置。4符号验证程序有效验证过程的下一步包括根据前一节中描述的丰富表示定义一个在断言语言上工作的符号前导运算符让我们首先介绍两个原子公式（具有不同变量）的多集之间的统一首先，对于原子公式A=p（x1;：;xk）和B=q（y1;：;y1），我们使用A = B作为约束x1= y1;：x k= y k的简写，假设p = q和k = 1。统一的定义如下。定义4.1设M=A1j：jAn：n，N=B1j：jBm：n为两个约束组态.我们说，如果M=N，则M=N，并且约束条件为：ni= Bjii=1是可满足的，j1;：; jn是1的置换;：;n。下面，给定E（例如，规则、约束或约束配置），我们称之为E0E的一个变体，如果E0 是通过将重命名的应用于E而获得的，即，E0=（E）（重命名是从E的变量到新变量的映射）。定义4.2[Pre运算符]运算符Pre在包含约束多集（具有不相交变量）的集合S上定义如下P re（S） =f（AN：9x1 ：xk：k）j（A！B：（）2R; （M：）2S;M04MB04B（M0：λ）=λ（B0：λ）;N=MM0和x1;：;xk是所有不出现在ANg中的变量：让我们举一个应用的例子。例4.3考虑约束配置p（x;y）！q（x;y）：x0;y=1;79设q（u;w）：u=1;w0，Pre（S）应包含p（x;y）：x=1;y=1以及p（x;y）jq（u;w）：x0;y=1;u=1;w0例如，在一个实施例中，p（4;1）jq（ 1; 5） re写入q（4;1）jq（1; 5）2[[S]]。后一个约束配置可以通过在将Pre应用于S时设置M0=B0=（空多集）来获得。新经营者享有以下财产。定理4.4（[15]）设hP;C;I;Ri是一个MSR（C）规格，S是一组约束构形（变量互不相同）. 然后[[Pre（S）]]= Pre（[[S]]）。为了定义一个符号可达性算法，我们仍然需要一个约束配置之间的比较算子。我们接下来讨论它应该满足的一般要求。定义4.5设hP;C;I;Ri是一个MSR（C）规格. 我们称之为关系在约束配置之间的v m（M M v mN暗示[[N]][[M]]。N;：）当每一个基于这个定义，我们可以定义一个符号向后可达性过程，我们可以使用它来检查安全属性，其否定可以通过向上闭合的配置集来在我们的设置中，我们可以将向后可达性算法（其对约束系统C和蕴涵关系vm是参数化的）重新表述如下。定义4.6Gi如果MSR（C）规范hP;C;I;Ri，约束配置的蕴涵关系v m，以及表示一组不安全状态的约束配置的集合U（具有彼此不同的变量），则符号向后可达性过程包括以下两个步骤：(i) 我们首先计算Pre（U）：从U开始，我们重复地将Pre应用于所有存储的约束配置。当不可能存储新的约束配置时（即，对于每个新的受约束配置M，我们已经计算了N，使得N vm（ M）;(ii) 如果不动点计算终止，则我们检查表示系统初始状态的初始配置I不包含在所得到的约束配置集合的表示中（即，I\[[Pre（U）]] =（掌声）。该算法的伪代码在图中给出。六、一般来说，算法不是终止的，因为有可能将不可判定的可达性问题（例如，对于两个计数器机器）编码为通用MSR（C）规范的验证问题。[18]如果我们能;80手术前（U：约束配置集）S：=U;R：=;而Sdo开始从S中移除（M：N）;如果没有（N：）2Rs：t：（M：）蕴含（N：），则将（M：）加到RS：=S[Pre（fM：）;endif结束结束语：见图6。符号向后可达性证明了vm是良拟序，则前面的过程是计算Pre（[[U]]）的完全算法.为了检查安全性，我们还需要与初始状态的交集的空性测试是可判定的。5CLP中的实施大多数CLP系统可以自然地用作本文所讨论的验证方法的实现平台CLP系统，如Sicstus Prolog的clp（Q，R）库，提供了符号数据结构来表示基于多集的规范语言和封装运算符，用于在对象级别处理约束这些功能使我们能够实现一个原型，其中MSR（C）规范通过单元子句表示，单元子句将术语与变量和约束相结合，例如：r（[p（X）;q（Y）];[r（Z）;t（W）];fX>Y;Z =Y;W = Y +1g）：这里，多集被表示为原子公式的列表，如[p（X）;q（Y）]，并且约束被表示（遵循clp（Q，R）语法）为线性算术原子约束的列表，如fX>Y; Z= Y; W = Y +1g。在这种设置中，符号前导和蕴涵算子可以通过使用统一（处理多集匹配）和查询约束求解器（检查可满足性，投影和蕴涵）自然81这样，我们必须能够将约束从未解释的术语转换为活动对象。此外，我们必须能够检索约束求解器产生的结果（可以将其视为将其输出放在约束存储中的oracle）。clp（Q，R）库为这类计算提供了特殊的内置谓词。具体来说，它提供了一个谓词，在输入中给定一个约束，此外，它还提供了可用于定义（以类似的输入输出方式）单个变量上的投影使用这些功能，我们已经定义了一个库处理（套）约束配置，我们已经将其纳入一个最少的不动点引擎与entailment作为终止测试。该原型已在几个应用程序中使用，如下节所述。6应用作为第一个应用程序，我们研究了互斥性质的不同formula- lations的门票协议。如[10]所示，即使对于只有2个进程的系统配置，该协议也具有无限状态空间。我们已经考虑了一个多客户端，单服务器配方，即与任意但有限数量的动态生成的客户端，但一个单一的共享资源，和多客户端，多服务器系统，其中客户端和服务器都是动态创建的。这两个例子都是使用带有线性约束的多集重写规则建模的，这些规则支持数据变量的增量和减量我们的模型忠实于算法的原始公式，因为我们没有抽象出附加到单个客户端的全局和局部整数变量，这些变量实际上仍然可以无限增长。使用我们的符号向后可达性过程结合抽象的动态使用，我们已经自动验证了两个模型对于任何数量的客户端和服务器以及任何局部和全局变量值都是安全的。我们的方法的第二个应用是分析Li和Hudak在[24]中提出的虚拟共享内存的一致性协议，并在[20]中进行了分析。使用我们的技术，我们发现在[20]中提出的有色Petri网模型中存在不一致性。在纠正错误后，我们自动验证了一个新的协议模型，其中线程、处理器和虚拟内存页面的数量是无界参数[8]。最后，我们自动验证多处理器系统的一致性协议（M.S.I.，法医鉴证科Synapse），其中处理器、缓存线和内存位置的数量作为无界参数[15]。我们目前正致力于应用这种方法来验证的安全和认证协议和抽象的并发程序。827相关作品我们的工作受到[2，4]方法的启发，其中存在区域被提出作为参数化时间Petri网的配置的符号表示。然而，在我们的框架中，我们考虑的问题和约束系统，不依赖于时间的概念。有限状态过程的网络可以使用[7，12，23]的自动机理论方法进行分析，其中全局状态集表示为规则语言，转换表示为语言上的关系。然后，可以使用具有特别加速或自动化抽象技术的自动机上的操作来执行从自动机理论的方法，在我们的设置中，我们处理参数化系统，其中各个组件的局部变量的范围超过无界值。前面的特征也将我们的方法与[5]的不可见不变量方法相反，我们在这里遵循符号模型检查的范式与丰富的断言语言[23]，试图隔离向后可达性终止的可判定类。这两种方法可用于使用不同的观点来解决类似的问题我们的想法与以前连接约束逻辑编程和验证的工作有关在这种设置中，转换系统通过CLP程序进行编码，CLP程序用于对系统的全局状态及其更新进行编码。我们通过使用多集重写和约束来细化这个想法，以局部指定对全局状态的更新。约束多集的概念是[16]中约束原子概念的推广。规则的局部性允许我们考虑丰富的表示（向上闭包）而不是平坦的表示（实例），例如，在[16]中。这样，我们就可以将方法提升到参数化的情况。最后，使用约束，向后可达性，结构不变量和更好的准序似乎都是将我们的混合方法与基于多集和AC重写技术的经典方法区分开来的因素（参见例如[11，26]）。引用[1] P. A. Abdulla，K. Cer ans，B. Jonsson和Y.- K. 是的无限状态系统的一般判定性定理在Proceedings 11 th Annual International Symposium on Logic in ComputerScience（LICSIEEE计算机学会出版社.[2] P. A. Abdulla和B. 琼森时间进程的网络。在B. Steffen ， 编 辑 ， Proceedings 4th International Conference on Tools andAlgorithms for Construction and Analysis of Systems（TACAS史普林格出版社[3] P. A. 阿卜杜拉湾琼森协议验证中的通道表示Proc. CONCUR 2001，LNCS2154，第1-15页。Springer，2001年。83[4] P. .A. Abdulla和A.尼勒恩。《BetterisBetterthanWell：OnEficientVerificationofInfinite-State Systems》（英语：Eficient在Proceedings 15 th Annual InternationalSymposium on Logic in Computer Science（LICSIEEE计算机学会出版社.[5] T. Arons，A. Pnueli，S. Ruah，Y. Xu和L. D.扎克自动计算归纳断言的参数化验证。In G.贝里，H。来吧，A. Finkel，编辑，Proceedings 13th International Conference on Computer AidedVerification（CAV史普林格出版社[6] A.布阿贾尼湾Jonsson，M. Nilsson和T.图伊里 定期模型检查。在E. A. Emerson和A. P. Sistla，编辑，Proceedings 12th International Conference onComputer Aided Verification（CAV史普林格出版社[7] M. C.布朗，E。M. Clarke，O. Grumberg.具有多个相同有限状态过程的网络的推理。信息与计算81（1）：13[8] M.博扎诺湾德尔赞诺超越参数化验证在Proc. TACAS[9] M.博扎诺湾德尔赞诺基于失效的协议的自动验证。将在2002年7月CAV '02号文件[10] T.布尔坦河Gerber和W. Pugh.基于Presburger算法的无限状态系统符号模型检验 。 号 手 术 Grumberg ， 编 辑 ， Proceedings 9th International Conference onComputer Aided Verification（CAV史普林格出版社[11] I. Cervesato，N.A. Durgin，P.D.林肯，J.C. Mitchell和A.谢德罗夫协议分析的Meta符号。In R. Gorrieri，编辑，第12届计算机安全基础研讨会（CSFW[12] E. Clarke，O. Grumberg，S. Jha.参数化网络。TOPLAS19（5）：726[13] G.德尔赞诺参数化缓存一致性协议的自动验证。在大肠A. Emerson和A.P.Sistla ， 编 辑 ， Proceedings 12th International Conference on Computer AidedVerification（CAV史普林格出版社[14] G.德尔赞 诺多维参 数系统的 断言语言 。In R. Mayr， editor，ProceedingsWorkshop on Verification of Parameterized Systems（VEPASElsevier Science.[15] G.德尔赞诺具有无界局部数据的参数化并发系统的自动验证。技术报告。Dipartimento di Informatica eScienze dellhttp://www.disi.unige.it/person/DelzannoG/papers.html84[16] G. Delzanno 和 A. Podelski CLP 中 的 模 型 检 查 。 In R. Cleaveland ， 编 辑 ，Proceedings 5th International Conference on Tools and Algorithms for Constructionand Analysis of Systems（TACAS史普林格出版社[17] J. Esparza ， A. Finkel 和 R. 迈 尔 广 播 协 议 的 验 证 。 在 Proceedings 14 thInternational Symposium on Logic in Computer Science（LICSIEEE计算机学会出版社.[18] A. Finkel和P.施诺贝伦到处都是结构良好的过渡系统Theoretical Computer Science，256（1-2）：63[19] F. Fioravanti，A.佩托罗西湾普罗耶蒂用程序变换验证无穷状态系统的集合。在Proc. LOPSTR55-66，2001年。[20] K. 菲 斯 勒 角 吉 罗 分 布 式 共 享 内 存 一 致 性 协 议 的 建 模 与 模 型 检 验 。 在Proc.ICATPN 1998中，pag. 84-103，2001年。[21] L. 弗里堡约束逻辑程序设计在模型检测中的应用以. Bossi，编辑，Proceedings9th International Workshop on Logic Program Synthesis and Transformation（LOPSTR史普林格出版社[22] J. Jaffar和J.L.拉塞兹约束逻辑编程在Proceedings 14th Symposium on Principlesof Programming Languag