µCRL工具集：抽象解释和模态转换系统的实现

理论计算机科学电子笔记133（2005）295-313www.elsevier.com/locate/entcs用于µCRLJaco van de Pol Miguel Valero Espada1，2Centrum voor Wiskunde en Informatica荷兰阿姆斯特丹摘要本文描述了一个工具包，该工具包有助于生成用µCRL语言编写的过程代数规范的抽象近似。抽象由模态标记转换系统表示，它是具有可能和必须模态的混合转换系统。该方法允许推断（基于动作的）µ演算中表达的安全性和活性属性的满足或反驳。该工具支持状态和动作标签的抽象，允许处理无限分支系统。关键词：抽象解释，模态转换系统，抽象模型检查，µCRL工具集。1介绍分布式系统的自动验证受到众所周知的状态爆炸问题的限制抽象是减少此类系统复杂性的有效方法。从一个具体的规范中，可以提取一个抽象的近似，它保留了原始的一些有趣的性质。在[32]中，我们提出了抽象µCRL [16]规范的理论框架。µCRL是一种结合了ACP风格处理代数[3]和抽象数据类型的语言。在本文中，我们将描述实现该理论的工具包。1电子邮件：{vdpol，miracle}@ cwi.nl2由荷兰科学研究组织NWO的嵌入式系统研究计划PROGRESS、荷兰经济部和技术基金会STW部分支持，授予CES. 5009。1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.08.070296J. van de Pol，M.Valero Espada/Electron.注意Theor。Comput. Sci. 133（2005）295在语义上，抽象由模态标记转换系统[23]表示，这是一种混合转换系统，其中转换被标记为动作和两种模态：可能和必须。可能的变迁决定了作为系统某些细化的一部分的动作，而必须的变迁则表示必然出现在所有细化中的那些。这两种模态的使用允许从抽象到具体的系统中推断出（基于动作的）µ-演算[22]中所写公式的满足或反驳。为了将抽象解释技术应用于现实系统，先前开发的理论的实施是不可或缺的一有不同的抽象方法可用于验证方法。例如，变量隐藏或逐点抽象，首先，指定的某些变量的值被认为是未知的，随后，当抽象变量上有谓词时，额外的非确定性被添加到系统中。另一种自动化抽象技术是所谓的谓词抽象，其中只有某些条件的值被保留并在指定的依赖谓词上传播程序切片是一种尝试消除规范中与当前验证无关的所有部分的技术最常见的抽象技术包括在较小的数据域上解释具体规范。用户选择要抽象的变量集，并提供一个新的抽象域，该域反映原始域的某些方面。这种技术需要创造性的人机交互，以选择适合抽象的系统部分，并提供相应的数据域。此外，用户必须确保抽象的解释满足了一些所谓的安全要求。我们的工具实现了自动逐点抽象，而且，帮助用户创建自己的抽象。 该工具支持使用数据抽象的两种主流技术。一个是由Long，Grumberg和Clarke [6，24]提出的，其中具体和抽象数据域通过同态函数相关，另一个是基于Cousots的抽象解释理论（我们使用抽象解释与大写来还实现了一个提升机制，它允许从同态自动构建伽罗瓦连接，参见[28]。标准的抽象框架只基于状态的抽象，这使得它们无法处理带有动作标签的无限分支系统。我们的工具的一个独特功能是它允许抽象J. van de Pol，M.Valero Espada/Electron.注意Theor。Comput. Sci. 133（2005）295297一状态和动作标签。在实现中，我们尽可能地特别是，我们将Modal-LPE编码为LPE，将Modal-LTS编码为LTS，以便重用µCRL和CADP工具集。我们还提供了一种新的方法，减少三值模型检测问题的两个2值模型检测问题。本文的结构如下：首先，我们介绍了抽象解释的基本概念，然后，我们描述了我们的工具的主要功能。随后，我们给出了一些案例研究，已使用该工具进行了分析的简短描述。本文最后与其他相关工具进行了比较。2预赛2.1变迁系统一个系统的语义可以通过标签转换系统（LTS）来捕获我们假设状态的非空集合S，连同转移标签的非空集合Act，则：定义2.1一个传递是一个三元组s→asJ，其中ha∈Act且s，sJ∈S。We定义一个标签转换系统（LTS）为元组（S，Act，→，s0），其中S和Act如上所定义，→是一个可能无限的转换集，S中的s0是初始状态。基本上，s→asJ表示状态s可以通过x而被转换到S J。一个行动的结束A.为了对抽象进行建模，我们使用了一种不同的结构，允许以更合适的方式表示具体系统的近似值。在模态标记变迁系统（ModalLabelled Transition System，简称MTS）中，变迁有两种模态，它们可以和必须表示细化中可能和必要的步骤。这一概念是由Larsen和Schloss提出的[23]。正式定义通过考虑两种模态扩展了LTS的定义。定义2.2模态标记变迁系统（Modal-LTS）是一个元组（S，Act，→may，→must，s0），其中S，Act和s0与前面的定义相同，并且→may，→must可能是以下（可能或必须）变迁的有限集合：J J形式s→xs，其中s，s∈S，a∈Act，x∈ {may，must}。 每must-transition是一个may- transition（→a必须 →a可能）。从LTS所描述的具体系统，我们可以通过将具体状态和动作标签与抽象状态和动作标签相关联来生成它的抽象。给定抽象关系，我们构造了具体关系的双重近似298J. van de Pol，M.Valero Espada/Electron.注意Theor。Comput. Sci. 133（2005）295系统建模的模态-LTS。可能的转变对应于原始的过度近似，而必须的转变对应于欠近似。在[32]中，我们已经提出了完整的抽象形式框架，现在我们给出一个例子（见图1）来介绍基本的直觉（注意，我们使用小写表示具体状态和具体动作标签，大写表示抽象状态和动作标签;没有源的箭头表示初始状态）。如果所有与抽象状态S相关的具体状态都有到与抽象状态SJ相关的具体状态的转换，则在S和SJ之间必须有转换。因此，在图1中，我们有抽象的必须转换S0→必须S0和S1→必须S2。如果存在与抽象状态S相关的某个具体状态，并具有到与抽象状态SJ相关的另一个状态的转换，则在S和SJ之间存在可能的转换。在图中，这些抽象的转换由虚线箭头标记动作标签也可以抽象，在示例中，具体标签：{a0，a1}映射到抽象标签A，{b0，b1}映射到B，如图所示。无论何时有一个必须过渡，也有一个可能的，我们不明确地画这样的案件。2.2过程方程µCRL是一种用于指定协议和分布式系统的正式语言用代数的方式。一个µCRL规范由两部分组成：一部分指定数据类型，另一部分指定进程。一个进程的规范是由来自一个ActNames集合（简称ActN）的动作名、递归变量和进程代数运算符构成的。动作和递归变量携带零个或多个数据参数。在µCRL中有两个预定义的进程：δ代表死锁，τ是隐藏的操作。它们从不携带数据参数。B抽象国家抽象国家具体转换抽象可能转换抽象必须转换Fig. 1. LTS的模态抽象示例S0a0级a0级一S1的1B1a0级b0的B一b0的S2J. van de Pol，M.Valero Espada/Electron.注意Theor。Comput. Sci. 133（2005）295299流程由流程术语表示，流程术语描述了操作可能发生的顺序。流程使用以下方法构建使线性矩阵运算符s：p·q，其中n是p+q和p+q上的一个组合序列非确定性选择，求和d：Dp（d）提供了可能的无限在数据类型D上的选择，并且具有数据类型Bool的数据项的条件构造pbDq在b时表现为p，在<$b时表现为q。 并行组合pq交错p和q的动作;此外，来自p和q的动作也可以同步到通信动作。数据类型（或排序）由一个签名组成，其中声明了一组函数符号和一组公理。对于每一个指定，我们假设存在布尔值（Bool），以及常量true和false（T和F）及其标准函数。[16]中给出了µCRL的语法和语义每个µCRL规范都可以通过线性过程方程进行编码：ΣX（d：D）=Σa（fa（d，ea））.X（ga（d，ea））ca（d，ea）Dδ（LPE）a∈ActNea：EaLPE是消除了并行组合的系统的所有可能交织的简洁表示在定义中，d表示向量[d0：D0，.，dn：DN]，表示系统在每个时刻的状态。我们使用关键字init来声明d值的初始向量。该过程由有限个被加数组成。 每个被加数都有一个listeaof local variables [ea0，...， （一）（二）（三）（四）（五）（五）（六）（六）（七）（八）（八）（ EaM]，并且它具有以下形式：条件ca（d，ea），如果条件的评估为真，则过程执行具有参数fa（d，ea）的动作a，并且将移动到新的状态ga（d，ea），其是D类型的项的向量。fa（d，ea）、ga（d，ea）和ca（d，ea）是在参数上递归建立的项局部变量和函数符号f在数据规范中定义。每个LPE对应一个标记转换系统（LTS），它代表系统的全部行为。由LPE描述的系统的语义由以下规则给出• s0= initlpea（d）→s如果存在ea∈Ea使得ca（s，ea）=T，ga（s，ea）=s′且d=fa（s，ea）基本上，抽象过程由原始规范到中间格式（Modal-LPE）的符号转换组成，该中间格式对模态抽象进行编码。模态-LPEs捕捉到了抽象解释所产生它们允许一个简单的过渡，• S′300J. van de Pol，M.Valero Espada/Electron.注意Theor。Comput. Sci. 133（2005）295一组状态和一组动作标签。ΣX（d：P（D））=Σa（Fa（d，ea））.X（Ga（d，ea））Ca（d，ea）Dδ（MLPE）a∈ActNea：Ea其定义类似于线性过程方程，不同之处在于状态由抽象值的幂集列表表示，对于每个Ca，返回一个非空的布尔值集，Ga是一个非空的状态集，Fa也是一个非空的动作参数集。 每一个模态- LPE对应一个模态标记变迁系统.由模态LPE描述的系统的语义由以下规则给出：• S0=初始化mlpea（D）→必须SGa（S，ea）若存在ea∈Ea满足h在F∈/Ca（S，ea），则D=Fa（S，ea）且S′=a（D）→五月SGa（S，ea）如果存在ea∈Ea使得T∈Ca（S，ea），D=Fa（S，ea）且S′=下一节将描述应用进程代数规范的抽象解释的工具和方法。3工具包下图显示了从具体规范中提取抽象近似的不同可能性。（一）混凝土规范（LPE））混凝土系统（LTS）zz（四）z（三）zzzzv（5）zza（二）v抽象规范（模态-LPE））抽象系统（模态-LTS）从编码为LPE的具体系统中，我们可以：• 生成具体的转换系统（1），从中我们计算抽象（2）。即使最终的抽象是最优的，这个选项对于验证不是很有用，因为由于状态空间的大小，生成具体的• 通过解释抽象域上的具体规范，直接生成抽象模态-LTS（3）。该方案避免了具体过渡系统的产生。• S• S′′zJ. van de Pol，M.Valero Espada/Electron.注意Theor。Comput. Sci. 133（2005）295301• 首先，生成具体系统的符号抽象（4），然后提取抽象的转换系统（5）。通常，标准的抽象解释框架实现第二种方法（图中的箭头（3）），但是我们相信第三种方法（箭头（4））是可行的。(4)接着是（5））一个更模块化。模态-LPE充当可能经受新变换的中间表示。有几种工具和算法（见[4]）可以操作线性方程，例如符号模型检查，状态空间减少，消除死代码，连续性分析。. .3.1工具概述下图描述了工具架构，其主要组件包括：抽象派。它负责完成从LPEs到Modal-LPEs的符号转换.它获取线性格式的µCRL规范，通常还有一组要抽象的参数和变量，然后生成一个新的规范。新的规范是抽象的骨架，它必须通过添加抽象数据规范来完成。该工具允许使用不同的抽象方法（同态，伽罗瓦连接和提升同态），所产生的规范将取决于用户抽象加载器。 它负责管理数据规范。从模态-LPE骨架，加载器可以导出用户必须提供的抽象签名以便完成指定。它还用于从外部文件导入抽象数据类型，并通过隐藏变量来生成自动抽象。正如我们之前所标记的，抽象解释必须被证明是正确的，该工具生成抽象函数必须满足的安全标准。有些安全要求可以使用µCRL定理证明器自动证明正确，其他则需要人工交互。抽象模型从抽象产生的过渡系统表示原始的双重近似。 我们使用三值逻辑来推断性质的满足或反驳。 三值模型检验问题可以转化为两个标准的二值问题。因此，可以使用现有的模型检查工具。动作标签可以被抽象。因此，必须根据抽象动作标签来抽象公式 由于公式的抽象性，在某些情况下，我们无法推断出具体公式的模型检验的准确结果，在3.4节中，我们提供了模型检验的指导，302J. van de Pol，M.Valero Espada/Electron.注意Theor。Comput. Sci. 133（2005）295抽象库来推断结果图二. 工具架构3.2抽象器抽象器将数据项替换为它们的抽象对应项。用户可以选择要抽象的参数和变量，然后抽象在规范的数据项上传播具体的函数符号f：X→ Y在需要时被它们的抽象形式所取代，抽象库定理证明器安全条件用户定义抽象抽象加载器例示器MLPE要抽象的参数变量不完全MLPEµCRL工具抽象器µCRL工具µCRL工具LPEMLTs式梅公式抽象模型必须公式是，不可能的问题模型检查器必要的问题J. van de Pol，M.Valero Espada/Electron.注意Theor。Comput. Sci. 133（2005）295303一般来说，有以下形式：abs F：abs X→ P（abs Y）。 让我们考虑一个非常简单的例子：ΣX（l：List）=write（b）.X（cons（b，l））lt（len（l），MAX）Dδ+b：位read（head（l））.X（tail（l））lt（0，len（l））Dδ线性过程指定一个有界缓冲器。进程可以在执行写或读操作之间进行非确定性选择仅当缓冲器未满时才能执行写入，即，模拟缓冲器的列表的长度小于最大长度（MAX）。如果缓冲器不为空，则可以执行读取操作在第一种情况下，状态参数通过将一个新的位连接到列表中来更新;在第二种情况下，列表的第一个元素被删除。混凝土规范具有以下签名：• 缺点：位×列表→列表• len：List→Nat• lt：Nat×Nat→Bool• 头：列表→位• tail：List→List如果用户选择要抽象的参数l，那么抽象的传播将产生以下签名（关于转换规则的完整列表，请参阅技术报告[30]）：• abs cons：Bit× P（abs List）→ P（abs List）• abs len：P（abs List）→ P（Nat）• lt：P（Nat）× P（Nat）→P（Bool）• abs head：P（abs List）→P（Bit）• abs tail：P（abs List）→ P（abs List）为了完成指定，用户必须提供ab-list的域，abs List，具体域和抽象域之间的关系以及新函数的定义（我们将在下一节中给出一个例子）。通过对非抽象的值执行逐点应用，工具自动提供了操作值集所需的所有函数。该工具允许使用两种主流技术来关联具体和抽象域：同态和伽罗瓦连接。在同态方法中，具体的数据值通过以下方式与单个抽象值相关：映射函数H。在伽罗瓦连接方法中，一个具体的数据值可能与几个抽象值相关一般来说，抽象的-304J. van de Pol，M.Valero Espada/Electron.注意Theor。Comput. Sci. 133（2005）295main被构造为晶格。 格中的顺序决定了抽象值的精度等级。为了定义伽罗瓦联络，除了有序域之外，我们还需要一个抽象函数α和一个具体化函数γ。一般来说，后一种方法保留了更多关于原始系统的信息，但使用同态技术可以更大地减少状态空间。此外，同态方法对于用户来说直观上更容易，因为根据值之间的映射比根据格之间的伽罗瓦连接更容易思考。抽象器支持使用这两种方法，也支持它们的组合，包括提升同态到伽罗瓦连接。在实践中，这种可能性是非常富有成效的，因为它允许用户只提供具体和抽象数据域之间的映射以及抽象函数的定义。该工具自动地将结构提升到伽罗瓦连接。详情请参阅[30]。模态线性过程方程可以转换回标准的线性过程方程.这允许重用设计用于操作LPE的µCRL工具。为此，我们首先通过添加两个后缀来扩展action标签 。 设 ActNames 是 Modal-LPE 的 动 作 标 签 的 集 合 ， 我 们 定 义ActNamesmay/must={a may|a∈ActNames}{a必须|a∈ActNames}。然后，我们重复为每个被加数在模态-LPE的基础上，提出了两个新的模态-LPE，一个用于可能跃迁，另一个用于必须跃迁。 这些新的被加数是按照以下模式构建的→下面介绍。我们用Ga表示Ga的元素的种类（同样成立→对于Fa）。 伽罗瓦连接和提升同态的模式是：ΣX（d：P（D））=Σa may（Fa（d，ea））.X（Ga（d，ea））a∈ActNea：Ea成员（T，Ca（d，ea））Dδ+Σ Σa必须（Fa（d，ea））.X（Ga（d，ea））（MLPE至LPE（GC））a∈ActNea：Eanot（member（F，Ca（d，ea）DδJ. van de Pol，M.Valero Espada/Electron.注意Theor。Comput. Sci. 133（2005）2953050同态的模式是：ΣX（d：P（D））=Σ Σ Σa may（fa）.X（{ga}）a∈ActNea：Ea→ →fa：F ag a：G amember（T，Ca（d，ea））member（fa，Fa（d，ea））member（ga，Ga（d，ea））Dδ+ΣΣ Σ a必须（f）.X（G（d，e））（MLPE至LPE（H））a∈ActNea：Ea→fa：Faa a anot（member（F，Ca（d，ea））singleton（Fa（d，ea））member（fa，Fa（d，ea））singleton（Ga（d，ea））Dδ模式是从第2.2节中提出的模态LPE的语义中派生出来的。对于同态，我们要求过程的状态和动作的参数是单个抽象值，因为每个具体值只映射到一个抽象值。然而，对于伽罗瓦连接，我们允许它们是值的集合。对于上面的例子，使用伽罗瓦连接方法，结果LPE可以/必须是：X（I：P（abs List））=Σ写may（b）.X（abs cons（b，l））member（T，lt（abs len（l），{MAX}））Dδ+b：Bitwrite must（b）.X（abs cons（b，l））not（member（F，lt（abs len（l），{MAX}））Dδ+b：位read may（abs head（l））.X（abs tail（l））member（T，lt（{0}，abslen（l）Dδ+read must（abs head（l））.X（abs tail（l））not（member（F，lt（{0}，abs len（l）Dδ模态LPE和LPE可以/必须的等价性由以下命题给出：命题3.1设M是一个模态LPE，mL是对应的模态LTS（S，Act，→may，→must，s0）. 此外，设M可以/必须是M的等价LPE可以/必须，并且设L是其对应的LTS（S，Act可以/必须，→，s）。那么，对于所有的s，SJ∈ S，a ∈ActNames，哪一个可能是空向量d<$的参数，我们有：amay（d<$）→sa（d）J五月→五月• SJ306J. van de Pol，M.Valero Espada/Electron.注意Theor。Comput. Sci. 133（2005）295amust（d<$）→sa（d）J⇐⇒s →musts这一命题对两种抽象都成立。证据可以在[30]中找到。3.3抽象加载器抽象器返回抽象的框架，即一个不完整的模态LPE. 为了生成相应的模态LTS，用户必须通过提供抽象域和抽象函数的定义来完成模态LPE抽象加载器通过提供导入/导出机制和自动抽象生成器来帮助用户在前面的示例中，abs List可以由具有三个值{empty，one，more}的域来描述，确定列表何时为空，具有单个元素或更多，移除关于所存储的元素的值的信息。然后，用户必须提供映射H：List→abs List3，例如：• H（nil）=空，H（cons（b，nil））=1，H（cons（b，cons（b′，l）=更多此外，他必须提供抽象函数的定义，例如：• abs cons（b，empty）={one}，abs cons（b，one）={more}和abs cons（b，more）={more}• abslen（empty）={0}，abs len（one）={1}和abs len（more）={2，3，.，maxLength} 4• abs head（l）={b0，b1}• abs tail（one）={empty}和abs tail（more）={one，more}Loader的模式导出列出了完成指定所需的函数，我们记得操作集合所需的函数是由工具自动生成的。模式加载用于导入定义。模式auto自动执行排序和函数的逐点抽象。一个模态LTS，从一个抽象的模态LPE（上和下）生成近似原始系统，如果每对函数（f，abs F）满足一个形式要求。安全标准列表由Loader以µCRL证明器的格式生成[29]。对于上面的示例，将生成以下条件5：• b、l： H（cons（b，l））∈abs cons（b，H（l））3或α：P（List）→abs List取决于用户选择的抽象类型4具体列表被认为是有界长度（maxLength）。或者，也可以抽象排序Nat。[5]安全条件的形式也取决于抽象的类型• SJJ. van de Pol，M.Valero Espada/Electron.注意Theor。Comput. Sci. 133（2005）295307• 你好， len（l）∈abs len（H（l））• l：head（l）∈abs head（H（l））• 你好，H（tail（l））∈abs tail（H（l））3.4抽象模型检测为了把抽象解释技术整合到验证方法学中，我们必须提供公式对抽象系统的满足与它对具体系统的反映之间的关系。本节描述了同态方法的抽象模型检查过程，伽罗瓦连接可以以等效的方式定义。通常，该过程如下：(i) 用户给出一个具体的公式，在具体的系统中证明（从现在开始M）。(ii) 行为的参数在抽象化后，被抽象为具体的类，从而得到绝对值。(iii) 我们检查了抽象模型（abs M，由Modal-LTS描述）上的ABS的满意度。(iv) 将满意度的结果推到具体的系统中。正如我们将看到的，这些推论有一些限制。（步骤i）具体的属性由以下逻辑描述（这是基于无交互动作的常规µ演算的一个非常有表现力的子集[25] ） 。有三种类型的公式，动作（α），规则（β）和状态公式（α），由以下语法表示：α：：= T |F |¬ α |α1∧ α2|α1∨ α2|a（d<$）β：：=α|β1.β2|β1|β2|β∗|β+：：= T|F| ¬ϕ|ϕ1∧ϕ2|ϕ1∨ϕ2|[β] β-环己二烯|⟨β⟩ϕ|Y| µY.|νY.ϕa代表来自ActNames的action标签，d<$代表参数列表，可能为空当列表为空时，我们只写一个。a（d）匹配具有相同操作标签和完全相同参数的转换。T匹配所有带参数的动作，<$α匹配除与α匹配的动作之外的所有动作。F不匹配任何动作，它可以用<$T来表示。正则公式匹配动作序列; “代表国际联络员"|'是选择运算符，''是传递和自反闭包运算符，'+'是传递闭包运算符。状态公式的语义是标准的。[β]表示所有由匹配β的序列所作的延拓都满足。⟨β⟩ϕ states that exists at308J. van de Pol，M.Valero Espada/Electron.注意Theor。Comput. Sci. 133（2005）295可以′至少一个β序列满足µ和ν是最小和最大定点算子。为了重用CADP工具集，我们假设状态公式是无交替的。（步骤ii）正如我们在前一节中所示，在抽象过程中，动作参数可以被抽象和/或提升到集合。为了证明H（d），我们将其转化为绝对H（d），即用其抽象的对应物替换动作的每个具体参数，即a（d）将被重写为a（H（d））。（步骤iii）在[20]之后，在模态LTS上对抽象公式进行双重解释，即，将存在满足它的两组状态。 从实际的角度来看，一个有趣的事实是，3值模型检验问题可以很容易地转化为两个标准的2值问题。这允许使用现有的模型检查工具，如CADP工具集的评估器[13]。为了进行翻译，我们遵循[5，14]的思想。基本上，给定一个公式，我们会生成两个不同的公式，第一个公式用于确定系统何时必须满足某个性质，第二个公式用于确定系统何时可能满足某个性质。它们的结构与abs_names相同，但构建在ActNamesmay/must之上，而不是ActNames之上。为此，我们定义了两个递归算子Tmay和Tmust。 见下文，第一个的定义（T必须是对偶的）：• T可以（<$abs）=<$T必须（abs）• 将abs中出现的[β]替换为[βmust]• 将abs中出现的β替换为βmay• 对于其余的情况，T可以被向内推。β可以用α可以替换所有出现的α，定义如下：• 如果α = a（d<$），则α可能= a可能（d<$）。• 如果α=T，则α可以=T可以。它匹配所有可能的行动。• 如果α=F，则α可以=<$（T可以）。它匹配不可能的动作。Tmust（可能）等于Tmust。• 如果α=<$（α′），则α可以=<$α′可能是吧。它匹配所有可能不匹配五月这些转换是在线性时间内完成的。这种方法与Godefroid等人[14]使用的方法之间的区别在于，我们使用一个模型和两个版本的公式，而不是生成两个不同的模型并使用一个公式。一般来说，公式比系统小得多，而且它们的复制成本较低。αJ. van de Pol，M.Valero Espada/Electron.注意Theor。Comput. Sci. 133（2005）295309（步骤iv）抽象模型检查过程的结果给出3值逻辑：• 绝对M必然满足绝对M。• abs M可能满足absM，但不一定满足absM。• 绝对值M不可能满足绝对值M。在第一种情况下，我们能够推断出满足条件，即，绝对M|= Tmust（abs）M|= H绝对值在第三种情况下，我们能够推断出反驳，即，绝对M|= T可能（绝对值）M|然而，第二种情况并没有提供任何关于满足或反驳财产的信息。具体公式的满足或反驳的推论并不简单。原因在于，通过抽象化，我们丢失了关于具体转换的确切信息。上面，|= H定义了一个抽象公式对一个具体系统的满足。状态和正则公式的语义不变。我们用<$abs α）H表示满足抽象动作公式的具体动作的集合。语义如下：<$T）H=Act<$F）H=Act<$absα1<$abs α2）H=<$absα1）H<$<$absα2）H<$absα1<$abs α2）H=<$absα1）H<$<$absα2）H<$abs α′）H=Act\<$abs α′）HA（abs d））H={a（d）|H（d）= abs d}我们现在举一个例子。让我们考虑下图的系统b（d）1图三. 抽象模型检查的例子。抽象是通过将s0和s1映射到s0，将s2和s3映射到s1和d0来以及D1到D。 我们要证明以下性质：• “It is possible to do a transitions0|= a（d0）T。该公式的抽象形式是εa（d）εT，它对S0三次成立.因此，我们可以推断，存在x使得H（x）=d，对于d，a（x）<$T在s0中成立。换句话说，|=<$a（d0）<$a（d1）<$T这意味着s0|=a（d0）T或s0|=a（d1）T.S0a（d1）a（d）b（d1）s0S2a（d0）S1b（d0）S3S310J. van de Pol，M.Valero Espada/Electron.注意Theor。Comput. Sci. 133（2005）295• “It is not possible to do a transitions0|= [b（d0）] F.这个公式的抽象形式是[b（d）]F，它对S0平凡地成立。因此，我们可以推断，对于所有的x，使得H（x）=d意味着[b（x）]F在s0中成立。换句话说，|=[b（d0）<$b（d1）] F，这意味着s0|=[b（d0）] F和s0|=[b（d1）] F.在第一种情况下，由于抽象，我们得到的信息比我们要求的要少，我们不能推断出具体模型中在第二种情况下，我们有足够的证据推断出确切的结果。注意，在没有数据参数的动作标签的特殊情况下，abs **将等于**，因此抽象模型检查问题与仅基于状态抽象的经典理论一致。4案例研究该工具已被应用于几个案例研究的验证过程中，例如，JavaSpaces应用程序的研究[11，33]。JavaS-paces是一个协调体系结构，它实现了一个共享存储库，外部代理可以使用该共享存储库通过共享对象进行通信。它为实现可靠的应用程序提供了额外的支持。系统可能会使用事务、通知机制和资源分配超时。通过将共享空间的内容抽象为一些重要的值和外部代理的状态，我们可以证明100多个并行进程的一些安全性和活性属性，这是一种典型的JavaSpaces应用程序。典型的应用程序由一个计算密集型问题组成，该问题通过将其分解为许多可以并行执行的较小任务来完成。此外，我们还研究了一个用于起重卡车（卡车，铁路车厢，公共汽车和其他车辆）的真实分布式系统[15]。 该系统由多个升降机组成;每个升降机支撑被升降的卡车的一个车轮，并具有自己的微控制器。 在每部电梯上都有一些控制其运动的按钮。 属于系统的不同电梯的微控制器一个安全属性被证明对任何数量的电梯都是正确的。这两个案例研究记录在[27]该工具也被用来证明有界重传协议的活性性质BRP是Philips加密协议的简化变体，允许通过有损通道传输大型文件。文件被分成数据包，并由发送方通过通道传输。接收器确认每个传送的数据包。数据和数据--J. van de Pol，M.Valero Espada/Electron.注意Theor。Comput. Sci. 133（2005）295311确认信息可能丢失。发送方将尝试对每个数据包进行有限次数的重传。该协议有许多参数，例如列表的长度，最大重传次数和数据的内容，这些参数导致系统的状态空间是无限的，并限制了自动验证技术（如模型检查）的应用。通过抽象这些参数中的一些，可以成功地应用模型检查（参见[31]）。在不同的上下文中，该工具已被应用于对许多不同的系统执行简单的抽象（参见[26]）。5结论和相关工作最接近我们的现有工具是αSpin [12]，它提供了一个抽象PROMELA规范的接口。用户可以从库中选择抽象。该工具会产生系统的过度近似。Bandera工具集[17]实现了相同的抽象方法，此外它还提供了程序切片和数据依赖分析的算法，以便自动找到合适的变量进行抽象。Bandera从简单的Java程序生成PROMELA代码。FeaVer [19]和abC [10]通过隐藏变量来抽象C程序。第一个将代码翻译为PROMELA，此外，它还允许用户定义自己的抽象，后者通过实现GCC编译器的扩展直接抽象C代码。Java Path [18]、BeBop [2]和SLAM[1]使用谓词抽象。我们参考[9]，以获得抽象模型检查工具和技术的扩展概述。所有列举的工具都只能生成过近似，因此只能检查安全属性的满足情况。我们的工具支持µ-演算，因此，我们可以使用模糊的安全性和活性属性。此外，从LPE到Modal-LPE的转换允许在语法级别上对抽象系统进行推理，并将所有技术嵌入到现有的µCRL工具中。最后，一个其他工具没有提供的重要功能是抽象操作标签的可能性。有关该工具的更多信息，请访问：http://www.cwi.nl/~miguel/Abstraction/。引用[1] T. Ball和S. K.拉贾马尼自动验证接口的临时安全属性。SPIN，LNCS，第2057卷，第103-122页，2001年[2] T. Ball和S.K. 拉贾马尼Bebop：一个布尔程序的符号模型检查器在SPIN，LNCS，第1885卷，第113-130页312J. van de Pol，M.Valero Espada/Electron.注意Theor。Comput. Sci. 133（2005）295[3] J.A. Bergstra和J.W.克洛普 抽象的通信进程代数 TCS5（2），第77-121页[4] S.布洛姆G.，I. van Langevelde，B. L.， 和J.C. van de Pol.µ CRL工具集的新发展。在ENTCS，Elsevier，第80卷，2003年。[5] G. Bruns和P. Godefroid。基于三值时态逻辑的部分状态空间模型检测。见CAV，LNCS，第1633卷，第274-287页[6] E. M. Clarke，O. Grumberg和D. E.久了模型检查和抽象。在POPL，ACM，第342-354页[7] P. Cousot和R.库索 抽象解释：一个统一的格子模型，用于通过构造固定点的近似来静态分析程序。在POPL，ACM，第238-252页[8] D.水坝。模型检验的抽象解释和划分细化。埃因霍温理工大学博士论文，1996年。[9] D.水坝。软件模型检查中的抽象：原理与实践（教程概述和参考书目）。见SPIN，LNCS，第2318卷，第14-21页[10] D. Dams，W. Hesse和G. J. Holzmann。用abC抽象C。CAV，LNCS，第2404卷，第515-520页，2002年[11] E. Freeman，S.Hupfer和K.阿诺德JavaSpaces原则、模式和实践艾迪生-韦斯利，1999年.[12] M. M. Gallardo，J. Martinez，Pedro Merino，and E.皮门特尔αSPIN：使用抽象扩展SPIN。STTT，5（2-3），第165 - 184页，2004年。[13] H. Garavel，F. Lang，和R. Mateescu，An Overview of CADP 2001，In EASST Newsletter，vol. 4，pages 13[14] P. Godefroid，M. Huth和R. Jagadeesan.使用模态转换系统进行基于抽象的模型检验。见CONCUR，LNCS，第2154卷，第426-440页[15] J.F. Groote，J. Pang和A.G. 武特斯 起重车分布式系统分析。InJune，56（1-2）：21-56，2003.[16] J. F. Groote和A.庞塞µCRL的语法和语义。在ACP，计算系列研讨会，第26-62页[17] J. Hatterygov，M. B.德怀尔角S.帕萨雷亚努和罗比Bandera抽象工具的基础。在计算的本质，LNCS，卷。2566，第172[18] K. Havelund和J. Skakkebaek。在Java验证中应用模型检查。在SPIN，LNCS，第1680卷，第216-232页[19] G.J. Holzmann和M.H. 史密斯 一种验证事件驱动软件的实用方法。在ICSE，ACM，1999年。[20