基于数据集的规范证明技术及其自动化验证和模型查找

理论计算机科学电子笔记95（2004）189-208www.elsevier.com/locate/entcs证明和基于数据集的规范J. - F. Cou chot a，1，F. Dadeau a，2，D. D'eharbeb，6，4，A. Giorgettia，3 和 S. Ranisec，5一LIFC，U. deFranche-Comt'e，BesanBesancon（France）bDIMAp/UFRN，纳塔尔（巴西）cLORIA INRIA-Lorraine，Nancy（法国）摘要我们提出了一种技术来证明不变量的基于模型的规格集理论的一个片段包含集合论构造的证明义务被翻译成一阶逻辑，等式被具有扩展性的数组理论（的扩展）增强。这种转换的基本思想是，集合由其特征函数表示，而特征函数又由一个以集合元素为索引的布尔数组编码。一个定理证明过程自动化的翻译所获得的证明义务的验证。此外，我们还讨论了如何从失败的证明尝试中提取子公式，并由模型查找器用于构建反例。具体来说，我们使用一个B规范的一个简单的进程调度，我们说明我们的技术。关键词：集合论，一阶逻辑与平等，决策程序，叠加，BDD，HARVey。1电子邮件地址：couchot@lifc.univ-fcomte.fr2电子邮件地址：dadeau@lifc.univ-fcomte.fr3电子邮件地址：giorgett@lifc.univ-fcomte.fr4电子邮件地址：david@dimap.ufrn.br5电子邮件：Silvio. loria.fr6由INRIA/CASSIS项目、CAPES赠款BEX 0006/02-5和CNPq赠款500473/2003-0提供部分资金。1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.04.012190J. - F. Couchot等/ Electronic Notes in Theoretical Computer Science 95（2004）189-2081介绍形式化方法越来越多地集成在硬件和软件工件的开发周期中。对于软件规范，业界愿意尝试严格的符号，如VDM [7]，Z [15]或B [1]。此外，定理证明和模型检查的组合越来越流行，以正式验证规范。定理证明履行了证明义务，需要系统在其规范方面的正确性;这是一项繁琐的活动，需要大量的用户交互，因为它通常是在不可理解的逻辑中进行的。例如，Z和B基于集合论（的变体）[1]这是众所周知的难以机械化。国家的最先进的定理证明器（如PVS7）只提供了有限的自动化，虽然大量的电子邮件已投入到自动化的例行推理任务。事实上，许多研究都涉及将选定理论的决策过程与更一般的推理活动结合起来[14]。定理证明的主要优点是它允许对软件系统中普遍存在的无限域进行推理。主要的缺点是很难判断一个性质是否因为假设不够强而没有被证明，或者是否只是在定理证明中需要一些额外的努力。模型检查包括寻找违反系统应该遵守的某些属性的反例。对于有限状态系统，它可以是自动的，而对于无限状态系统，它只能是半自动的（即搜索可能不会终止）。对于无限域，模型检查的主要缺点是它可以找到反例证明规范与系统矛盾，但它可能无法证明规范是正确的。在本文中，我们建议利用一阶理论[3，8]的决策过程设计的最新进展来构建自动和可扩展的工具，用于证明和调试基于集合的规范。我们的方法的关键思想是，在许多实际相关的情况下，只有集合论的片段被使用，这些片段可以被转换为等式一阶逻辑的可判定理论。为了测试我们的方法的可行性，我们选择了B方法的规范语言。然而，我们希望基本方法普遍适用于规范的基于模型的方法，该方法还包括其他符号，如Z或VDM。我们的方法的主要成分是四重的。首先，我们将B规范语言的一个选定子集转换为一阶扩充逻辑7 http://pvs.csl.sri.comJ. - F. Couchot等/ Electronic Notes in Theoretical Computer Science 95（2004）189-208191一 些集 合 论 的构 造 。 更 确切 地 说 ， 一 个B 规 范模 块 -- 称 为抽 象 机（AM）--被转换为一阶公式，根据其运算对AM变量的前后值之间的关系进行编码。这样的公式可以包含集合（具有特定结构）和选择的集合理论构造。 第二，前后代表--将系统的表示与AM的不变量一起平移转化为一组一阶证明义务（包含集合论构造），这意味着不变量对于AM是归纳（我们的方法的前两个要点在第2节中简要概述，因为它们是对现有技术的适应，例如：[1]）第三，我们消除了集合论的结构，在证明义务解释他们在一个扩展，具有可拓性的数组的可判定理论（第3节），见例如。 [3]的文件。这样的转换是基于这样的想法，即由集合s的元素索引的布尔数组表示s的特征函数。第四，我们预先处理由此产生的证明义务，以消除量化器，从而得到基础公式（第4.1节）。这种预处理包括用命题字母q彻底地替换量化的子公式，并将公理q惠函添加到背景理论中。后来，我们调用haRVey[8]-一个推理系统，能够证明的有效性，无量化器公式模方程一阶理论-以履行由此产生的证明义务（第4.2节）。如果一个公式被证明是有效的，那么我们将其报告给用户。否则，提取选定的子公式并将其传递给模型查找器（即采用公式并尝试查找其模型之一的工具），以便可以构建反例，然后由用户仔细检查，以了解公式未能被证明有效的原因（第4.3节）。相关工作。最密切相关的工作是[13，12]，因为它试图通过松散耦合AtelierB8与Alloy分析器9来结合最好的- orem证明和模型发现。主要的区别是，整个证明义务用于定理证明和模型发现，而我们使用定理证明来简化公式，以便只有一小部分（最终负责其无效性）被传递给模型发现者，从而大大简化这最后一项任务。有一些工作（例如[4]）使用最先进的定理证明器在基于状态的规范语言（如B，Z和VDM）中进行形式推理。这类著作的重点是从集合论到证明者使用的逻辑的翻译的合理性，而忽略了问题8http://www.atelierb.societe.com/index.html9http://sdg.lcs.mit.edu/alloy192J. - F. Couchot等/ Electronic Notes in Theoretical Computer Science 95（2004）189-208自动化，从而留给用户的负担，长期和繁琐的互动证明。相反，我们的工作集中在翻译集合论的一个片段，其中定理证明问题可以通过使用一阶方程理论的决策过程据我们所知，这是第一次提出使用数组理论的决策过程（的扩展）的想法，通过用数组表示集合的特征函数来机械化集合论（的片段）中的推理。由于篇幅有限，我们无法在本文中详细比较基于集合的规范（如AtelierB）的现有证明器。然而，4.4小节报告了一些初步证据，表明我们的方法在处理简单数据结构的大型规范类上优于AtelierB。2B规格说明和验证方法B方法有一个相关的规范表示法，称为抽象机器表示法（AMN）。这是一种基于状态的表示法，类似于Z或VDM，其特征在于赋值（：=）、条件（IF THEN ELSE）、多重赋值（||）和非确定性选择（ANY）[1]。粗略地说，AM由一些状态变量、初始化和一些可能改变状态变量值的操作组成 虽然B方法包括一个规范的细化和实现，我们在这里只考虑检查一个不变量是否通过初始化建立，并通过执行AM的所有操作来保存。暗示AM操作的正确性的证明义务和关于其候选不变量的初始化是在一个有效的过程（沿着[1]中的路线）之后生成的。例2.1（进程调度器）作为一个运行的例子，我们在上面说明我们的技术，我们考虑在[ 9 ]中介绍的进程调度器。虽然简单，但这个例子允许我们讨论在处理我们的技术所针对的AM类型时出现的典型问题，即，（大型）操作简单数据结构的AM其B规格的摘录如图1所示。在任何一个时刻，系统可能有一些进程准备好被调度，一些进程在准备好之前等待一些外部动作，并且可能有单个活动进程。每个进程都由一个标识符（从一组PID中取出）唯一标识。活动、就绪和等待的不变状态是PID的成对不相交子集，并且最多一个进程可以处于活动状态（这在进程的执行中强制互斥）。初始化要求所有进程都处于J. - F. Couchot等/ Electronic Notes in Theoretical Computer Science 95（2004）189-208193机器PSAM设置PID变量活动、就绪、等待不变ready_pid_active_pid_waiting_pid_ready_waiting=ready_pid_active=ready_active_waiting=ready_card（active）≤1初始化激活，就绪：=0，0||等待：=PID操作交换=如果激活/=等待THEN等待：=等待激活||如果准备就绪，则ANYPR WHEREPR∈ready THENactive：={pr}||准备：= ready-{ pr}端ELSEactive：=0结束结束... 结束语：Fig. 1. 一个过程的摘录。一开始的等待状态。图1只是显示了Swap操作，它允许AM通过将当前活动的进程与就绪的进程交换来进行演进，如果没有就绪的进程，则使系统空闲操作（如Swap）的规范是对预期状态修改必须满足的某些相关属性的描述。 为了正式表达这些属性，一种常见的技术是编写所谓的before-after谓词，该谓词将状态变量的值（即ready，waiting和active）与操作发生之前和之后的状态变量的值相关联（详见[1]）。为了写出这样的谓词，我们采用了这样的惯例，即在执行操作之后，通过启动相应的标识符来表示变量的值。下面的before-after谓词PSwap（r，w，a，rJ，wJ，aJ）指定了操作Swap：如果 a/=0则wJ=w<$a<$（1）如果r i = π，则πpr。（pr∈r<$aJ={pr}<$rJ=r−{pr}）elseaJ=rJ=r否则aJ=a<$rJ=r<$wJ=w其中，r， w， a， rJ， wJ，A表示就绪，等待，活动，就绪J，等待J和主动J。布尔条件连接词ifAthenBelseC194J. - F. Couchot等/ Electronic Notes in Theoretical Computer Science 95（2004）189-208交换酸盐（A<$B）<$（<$A<$C）其中A、B和C为式。我们使用这样一个结构是为了在before-after谓词中保持B规范的结构。 注意，非确定性选择运算符（ANY）由存在量化和多重赋值运算符（||）的连接。此外，未显式分配的状态变量将保留其先前的值。虽然这不在本文的范围内，但我们相信，我们的方法很容易适应其他B结构，如常数，机器参数和属性。不变的（cf。图1的INVARIANT子句）可以很容易地转换为以下谓词：(2)rpwpaprw=ra=aw=card（a）≤1，其中p是表示PID的常数;它缩写为Inv（r，w，a）。一旦一个操作和不变量都被谓词指定，我们就可以通过检查以下公式的有效性来证明该操作保留了不变量，该公式编码了在执行Swap之后Inv保持不变的事实，前提是它在之前保持不变（3）n，r，w，a，RJ，WJ，AJ. （In v（r，w，a）<$P（r，w，a，rJ，wJ，aJ）<$In v（rJ，wJ，aJ））。除了证明每个操作保持不变式Inv之外，还必须检查Inv是否满足初始化条件（参见图1的INITIALISATION 子句）。我们省略了相应的证明义务，因为这对讨论没有多大帮助证明义务--如（3）--应通过使用自动定理证明器来解除。通常，在支持B方法的当前可用的商业工具中，存在自动证明器不能履行的多个证明义务，因此开发者可以将证明器切换到交互模式并尝试手动地履行剩余的证明义务。 B方法实际上是由两个商业上有用的-强大的工具：B-Toolkit10和AtelierB。11虽然相当成功，这两种工具都不帮助开发者发现为什么某个证明义务没有被证明是有效的。在本文的其余部分，我们描述了一种技术来检查证明义务的有效性，并提供给用户的反例时，有效性检查失败。10http://www.b-core.com/btoolkit.html11http://www.atelierb.societe.com/index.htmlJ. - F. Couchot等/ Electronic Notes in Theoretical Computer Science 95（2004）189-2081953翻译基于集合的证明义务在第2节中，我们依靠读者在这里，我们定义了我们使用的集合论的简单版本，并解释了如何将其转化为一阶逻辑的适当扩展，使其具有相等性（参见。第4.2节）--一个检验方程一阶公式有效性的系统--可以用来履行这种证明义务（如果可能）。下面，我们假设一阶逻辑的常见语法和语义概念，等式如[10]中的例子我们说公式φ是满足模理论Tiφ T是满足的。3.1简单集合论为了简单起见，在本文中，我们考虑一个限制片段的集合论，我们表示为SSET。然而，请注意，我们的方法可以扩展到处理集合论的更有表现力的片段，例如带原子的遗传有限集理论（见[5]），它允许本原元素的集合，本原元素的集合的集合，等等。SSET是一个一阶排序逻辑的理论。它包含两个不同的排序符号ELEM和SET。它的术语集包含elem和SET排序的变量和常量符号。我们假设至少有一个常数的排序ELEM。区别常数是一个排序集项。 如果e是一个项，的排序ELEM，则{e}是排序集的项;此外，如果s1和s2是sortSET，则s1Das2也是sortSET的一个项，其中Da是二元函数符号（交集），（并集）和\（集合差）之一 我们也写{e1，.，en}作为{e1}··{en}的 缩写 。 SSET 的 原子 集 包 含以 下 形 式的 表 达 式： e1=e2， e∈s，s1<$s2，s1=s2，其中e，e1，e2是elem类的项，s，s1，s2是类集的项。文字，文字的布尔组合，以及可能的量化公式都是以通常的方式归纳定义的。此外，设Ax（SSET）是通过将以下公理添加到等式理论而获得（4）多效性。（<$E∈N），(5)谢谢（E∈ {E}），(6)P. E，F. （E/=FE∈ {F}），（7）S1、S2。（E∈S1< $S2惠（E∈ S1<$E∈ S2）），（8）S_1、S_2。（E∈S1< $S2惠（E∈ S1<$E∈ S2）），（9） S1、S2。（E∈S1\ S2惠（E∈ S1E∈ S2）），（10）S1，S2. （S1）S2优惠券E。（E∈S1<$E∈S 2）），（11）S 1，S 2. （S 1 = S 2惠益E。（E∈S1惠E∈ S2）），其中E，F是ELEM类的变量，S，S1，S2是集合类的变量.SSET的语义由一阶解释类给出196J. - F. Couchot等/ Electronic Notes in Theoretical Computer Science 95（2004）189-208SSSSSSSS满足Ax（SSET）中的每个公理。直观地说，我们正在考虑的集合论允许对具有非常简单结构的集合进行推理，即。集合（由排序集合的项表示），其是给定通用集合（例如，图1的示例中的集合PID）的子集，并且其元素（由排序元素的项表示）是原语。因此，例如，如果全称集合是整数的集合，则集合{1，2， 3}是有效的“不，不，不。请注意，SSET已经在许多实际验证问题涉及大型系统（比如一些B规范），这些系统操纵由原始元素集表示的简单数据结构。3.2具有可拓性设Ae是具有排序值、索引和数组的多排序理论，函数符号write（以下缩写为wr）和read（以下缩写为rd）分别为ARRAY×INDEX×VALUE−→ARRAY和ARRAY×INDEX−→VALUE此外，设Ax（Ae）是通过将以下公理添加到等式理论而获得的公理集（十二）（十三）A，I，J，E.（一）A，I，E. （rd（wr（A，I，E），I）=E），J=rd（wr（A，I，E），J）=rd（A，J）），(14)A，B. （一）（rd（A，I）=rd（B，I））A=B），其中A和B是排序数组的变量，I和J是排序索引的变量，E是排序值的变量。e表示一个签名，包含函数符号rd、wr和一组有限的（未解释的）函数符号。我们假设Ae的签名承认每个排序至少有一个基项。检查地面文字模Ae的合取的可满足性是可判定的（参见，例如，[3]）。3.3从集合论到数组论我们解释了如何将SSET的公式转换为Ae的（扩展），以便推理系统具有（参见。第4.2节）可以用来解除证明义务，这意味着AM的不变量是机器的归纳属性（沿着第2节中描绘的路线）。在（的扩展）中解释SSETe是基于使用特征函数来表示集合。这样的反过来，函数可以由布尔数组编码，布尔数组的索引是集合的元素。例如，集合s：={ 1， 2}可以表示为s[1] =s[2] =true和s[x] =false，对于所有不同于1和2的x。形式上，我们定义SSET（的基项集）到Ae（的适当扩展的基集）的翻译如下。一J. - F. Couchot等/ Electronic Notes in Theoretical Computer Science 95（2004）189-208197^^^您的位置：^^ ^您的位置：^^我们引入了两个著名的常数tt和elem类，并考虑了公理(15)tt/= 0.这样，价值的解释就是通常的真值集合。我们将排序符号ELEM和SET分别映射到INDEX和ARRAY我们假设排序数组存在一个可区别的常数符号mty（表示空集），并考虑公理（16）第一部分。（rd（mty， I）=0），其中I是排序索引的变量。我们将ELEM和SET的排序常量分别映射为INDEX和ARRAY的排序常量（区别常量mty映射到mty）。形式为{e1，...，.. 形式s1和s2的基本项（其中s1和s2是排序集的项）翻译如下。 首先，我们平移s1和s2让我们^1 和s^2是排序数组（分别）。然后，我们引入一个（17）第一部分。（rd（u，I）=tt惠（rd（s^1， I）=tt惠rd（s^2， I）=tt）），其中I是排序索引的变量。SSET的其余集合论构造（即，和\）以类似的方式处理。最后，对于排序数组的每个常数s（表示一个集合），我们考虑以下公理：(18)我是。（rd（s，I）=ttrd（s，I）=），其将特征函数s的余域约束为{tt，n}。下面，如果e是SSET的基础表达式（项、原子或公式），则e表示其平移。此外，我们翻译的基础原子SSET如下。形式为e∈s的基原子映射为rd（s，e）=tt。形式为s1<$s2的基原子被替换为新的命题字母q，并考虑以下公理：（19）q优惠I. （rd（s1， I）=tt<$rd（s2， I）=tt），其中I是排序索引的变量。最后，将e1=e2和s1=s2形式的基原子转化为e1=e2和s1=s2，其中e1是ELEM类项，si是集合类项，i=1，2。这个转换过程以显而易见的方式同胚地扩展到原子的布尔组合设φ是SSET的基公式，φ是SSET的平移.我们用BAe表示包含Ae、公理（15）、（16）以及同样多的变式的S s（17）、12和（19）根据需要， 根据新符号[12]包括可能相似的集合交和集合差的公理198J. - F. Couchot等/ Electronic Notes in Theoretical Computer Science 95（2004）189-208^^SSS^^^您的位置：SS^引入φ。通过使用这个符号，我们可以陈述以下事实（我们用可满足性来陈述它，因为我们的定理证明方法是基于反驳的;见4.2节）。理论m3.1φ是SSET i的可满足性模型，φ^是BAe的可满足性模型。草图（Sketch）我们证明，如果φ是satisfiable模SSET ，那么φ是satisfiable模BAe。另一个双对比度的含义是类似的，因此被省略。在SSET中，我们定义函数ins如下：（a）in s（e，s） ={e}和（b）in s（e，s） ={e} s，f或所有g轮项e和s的排序ELEM和SET，分别。很容易看出，我们可以通过穷尽地应用（a）和（b）作为从右向左的重写规则来消除φ中出现的每一个单例集函数{ }。这个过程显然终止，因为在规则的每次应用中，单例集函数的出现次数减少一次。设φJ为 所 得 的 基 础 公 式 。 现 在 ， φ 对 Ax （ SSET ） i 是 可 满 足 的 ， φJ 对 Ax（SSETJ）是可满足的，它是通过用以下公式替换公理（5）和（6）从Ax（SSET）得到的：（20）P.E.，S. （E∈ins（E，S）），（21）黄曲霉E、F、S. （E/=F<$（E∈ins（F，S）惠E∈S）），其中E、F是ELEM排序的变量，S是排序集的变量。事实上，（20）和（21）都是Ax（SSET）和ins定义的逻辑结果（即上面的事实（a）和（b））。然后，我们将SSET的基项映射扩展到BAe的基项，以考虑新定义的函数ins，如下所示：形式为ins（e，s）的基项映射到wr（s，e，tt）。下面是一个容易证明的引理。设t是特征函数{{}，{}}∈ E∈S 上的基项，其中E（re sp.S）是一个有限的 集 合 ， 集 合 了 一 些 元 素 （ 例如，SETT）andtdJbethetermont h e gnature{ins，n}{\displaystyle\mathbb{ins，n}}{\displaystyle\mathbb{ins ， n}}{\displaystyle\mathbb{ins ，n}{\displaystyle\mathbb {in s ， n}{\displaystyle\mathbb{ins ， n}{\displaystyle\mathbb{ins ，n}}{\displaystyle\mathbb {in s，n}{\displaystyle\mathbb {in s，n}}{\displaystyle\mathbb {in s，n}{\displaystyle\mathbb {ins，n}}{\displaystyle\mathbb{ins，n}{\displaystyle\mathbb{\displaystyle\mathbb{ins，n}{\displaystyle\mathbb{ins，n}{\displaystyle\mathbb {\displaystyle\mathbb {in s}{\displaystyle\通过穷尽地应用等式s（a）和d（b）消除{ }的所有出现而从t获得。这实际上并不等同于我。 作为花冠y，我们可以推导出，φ^j基本上等于φ^J。JeJLetφ是BAs的形式，其中是φ的转换。ITISEASYTO可以看出，Ax（SSET）J中公理的基础实例的平移都是Ax（BAe）的逻辑结果。 因此，通过上面的引理，我们有权得出结论：如果φ对BAe是不可满足的，那么φ对SSET也是不可满足的。Q关于基数运算符的注释（参见 图1）。让我们只考虑形式为card（s）=k的基态原子，其中s是分类集合的项，k是给定的数。 然后，我们可以替换形式的每个原子，J. - F. Couchot等/ Electronic Notes in Theoretical Computer Science 95（2004）189-208199S交换交换交换S交换card（s）= k，其中s ={f1，...，fk}，其中fi是elem类的新常数（对于i= 1，.， k）。在这样的规则的穷举应用之后，我们得到SSET的公式，其可以如上所述被翻译为BAe我们可以推广这种方法来处理任意的算术关系。例如，card（active）≤1可以重写为card（active）=0这反过来又重写为active={f1}，其中f1是一个新的类元素常数实施例3.2（方法详述-续）将（1）中的catePSwap转换为谓词P eq：如果a/=mty则wJ=w Ua（二十二）如果r曼天雨然后是bypr。（rd（r，pr）=tt<$aJ=wr（mty，pr，tt）<$rJ=wr（r，pr，tt））否则 aJ=mtyrJ=r否则aJ=a<$rJ=r<$wJ=w其中w，a，r和它们的素数版本是排序数组的变量。可以通过使用上述翻译来表达验证条件（3）中的集合论构造，从而获得公式(23) r，w，a，rJ，wJ，aJ. （Inveq（r，w，a）Peq（r，w，a，rJ，wJ，aJ）Inveq（rJ，wJ，aJ））（纯）一阶理论（等式），其中Peq如上所述，Inveq是Inv的翻译。如果我们通过反驳进行推理，定理3.1允许我们说（23）模BAe的否定的可满足性等价于（3）模SSET的否定的可满足性。很容易看出，在（23）的否定式中，变量r，w，a，rJ，wJ和aJ成为存在的当Peq中的变量pr仍然会被量化。作为因此，所有的变量都可以用Skolem常数代替，这样（23）的否定可以被认为是一个基础公式（见第4节，了解对量化器的更系统的处理）。最后一句话是合适的。对WS1S [6]有一定了解的读者可能想知道SSET是否可以转换为这样的逻辑，以便证明义务可以通过现有的工具（例如Mona[11]）来履行这个问题的答案确实是肯定的。然而，我们指出，在我们的应用程序中生成的证明义务通常非常大，因为原始AM很大。现在，Mona像所有基于自动机的工具一样解决了内存消耗出于这个原因，在实践中，莫娜似乎不适合处理一些最大的举证责任，在我们的200J. - F. Couchot等/ Electronic Notes in Theoretical Computer Science 95（2004）189-208eS交换SSSSSS应用程序（有关此问题的更多详细信息，请参见第4.4节）。如前所述，我们的方法可以扩展到处理更有表现力的集合理论。对于以MONA工具为目标的翻译，情况并非如此。由于WS1S逻辑只能处理原始元素（整数）和原始元素集合，因此在这种逻辑中编码原始元素集合的集合并不简单。我们的理论扩展到原始元素的集合等等，只要相应地扩展数组As的理论就可以了。4解除证明义务我们剩下的问题是检验一阶逻辑的等式公式，如（23），是等式理论的逻辑推论BAe（扩展Ae）。 为了做到这一点，我们通过反驳来推理，并证明S s公式的否定是模BAe不可满足的。实施例4.1（方法详述-续）为了证明义务（23），我们证明：(24) r，w，a，rJ，wJ，aJ. （Inveq（r，w，a）<$Peq（r，w，a，rJ，wJ，aJ）<$<$Inveq（rJ，wJ，aJ））是不可满足的模BAe。我们的基于反驳的定理证明技术有三个阶段。我们将在下面的小节中详细描述它们。4.1消除量化器我们展示了如何将一阶公式φ（可能包含量化器）模BAe的满足性降低到基础公式φg模理论EBAes. t.φ满足模BAeiφg满足S s模EBAe和BAeEBAe. 关键思想是将φ转换为通过用新公式替换φ的量化子公式，命题字母，并将其定义添加到公理Ax（BAe）中，以这样的方式，Ax（BAe）<$φ是满意的，如果Ax（BAe）<$φg是。s s s首先，预处理用“新鲜的”skolem常数a替换所有最外面的存在量化变量a然后，由于我们希望尽可能地保留公式的命题结构（以便在下一阶段可以被哈维利用），我们尽可能地向内移动量化器。为此，我们使用所有的规则将公式转换为前束形式13（详见[10]），但相反[13]一个公式是前束形式的，如果它具有结构Q1x1. 其中，Qi是λ或λ，xi是变量（i= 1，.，n），φ是一个无量化因子的公式，其自由变量为x1，...， xn.J. - F. Couchot等/ Electronic Notes in Theoretical Computer Science 95（2004）189-208201SSSSS交换交换SS方向例如，公式x。如果x不出现在φ中，则（φ）变换为（φx.φ）φ。在这一点上，我们用一个“新的”命题字母q请注意，如果有一个量化的子公式J出现在j中，我们不会递归地将上述过程应用于j，而是在以下级别停止的。这是一个启发式的决定，在实践中似乎会产生良好的结果设φg是通过穷尽地应用变换而获得的公式，上述和EBAe是通过将新命题字母的定义添加到BAe而获得的理论，如上所述。定理4.2φ满足模BAei（基本公式）φg满足-是可解的模EBAe。这个定理的证明依赖于Skolemization的基本性质（参见，例如[16]）。 这是一个例行的练习，因此省略了。例4.3（过程分析器-续）让我们考虑公式（24）。首先，我们将最外层的存在量化变量替换为Inveq（r，w，a）<$P eq（r，w，a，rJ，wJ，aJ）<$<$Inveq（rJ，wJ，aJ）.这是令人满意的i（24）是（由一阶逻辑的基本性质[10]）。14上式中的子公式Peq因为唯一的存在量化器不能进一步向内移动，我们用新的命题字母代替存在量化的子公式Q. 因此，我们得到以下等式如果a/=mty那么wJ=w Ua（如果rj=mty那么qelseaJ=mtyrJ=r）否则 aJ=a<$rJ=r<$wJ=w和公式q惠q pr。（rd（r，pr）=tt <$aJ=wr（mty，pr，tt）<$rJ=wr（r，pr，tt））加到Ax（BAe）上。4.2检查满足性剩下的问题是检验基公式φg模一阶理论EBAe的不满足性。我们通过调用haRVey15来解决这个问题，haRVey 15是一个基于以下方面的灵活和高效组合的工具：BDD和叠加定理证明（详见[8]）。 这个想法是[14]如果公式包含自由变量，我们取其存在闭包。15 http://www.lor ia. fr/e quipe e s/c as sis/s oftwar e s/h aR Vey202J. - F. Couchot等/ Electronic Notes in Theoretical Computer Science 95（2004）189-208SSSSSSS函数havey检查sat（EBAe：一阶理论，φg：基础公式）φa←−abs（fol2prop（φg））当φa/=φ d0时βa←−pick branch（φa）（ρ，π）←−检查sat分支（Ax（EBAe），prop2fol（βa））如果是，则返回yesφa<$−φa <$fol2prop（π）不返回端图二. HARVey的算法将基原子抽象为命题字母，然后让BDD表示φg的布尔结构（的抽象）。由于很容易从φg的BDD表示中提取其析取范式（DNF），我们检查DNF模EBAe中每个析取的满足性通过调用叠加定理证明器 在实践中，这一模式的细化，大大提高性能（基于生成合适的引理以简化BDD的能力）实际上在系统中实现。 为了建立检查一阶理论的满足性的程序，我们采用了[3]的基于叠加的方法。这允许许多决策（和半决策）过程的灵活实现，只需向叠加定理证明器提供理论的公理和待证明的文字即可。它也是[2，8]中所示的专门决策程序的有效替代方案。图2显示了基于haRVey的算法。设Atm是φg中不同基原子的集合，Atm是命题字母的集合S.T. Atm和PA tm的基数相等，且Atm=PA tm=N。 设atm2pl是从Atm到PAtm的双射函数。我们将从基一阶公式φg到命题公式的映射fol2prop定义为atm2pl到φg的同胚扩张。然后，abs获取fol2prop返回的比例公式，并构建其BDD表示φa。函数pick branch选择BDD φa中从根到标记为true的节点的分支（也称为真分支）; βa是命题字面量的合取。 我们假设prop2fol是fol2prop的逆，所以它的结果是一个基础一阶文字的合取。此外，我们要求检查sat分支（Ax（EBAe），β）=（λ，π）i λ π是下式的子公式：β，并且它对EBAe取模是不可满足的;因此，检查sat分支是一个决策过程检查是否地面文字的合取是satisfiable模EBAe与返回的输入文字的小子集是unsatisfiable的能力的问题。这样一组文字可以用来简化BDD，如图1中循环的最后一条语句所示二、我们考虑BDD中的分支，直到其中一个被证明是可满足的模EBAe（在这种情况下，我们返回φg是可满足的），或者BDD已被简化为φ（即，通过交错的不满意度检查，J. - F. Couchot等/ Electronic Notes in Theoretical Computer Science 95（2004）189-208203SBDD简化步骤。4.3为用户提供反例如果一个分支β被哈维发现是令人满意的，那么我们就可以用它作为起点来为所考虑的公式φg建立一个模型，即一个要证明有效的公式的反例（它是φg的否定）。请注意，这是一个优势w.r.t.建立整个公式φg的模型，因为分支通常要小得多。在初步研究中，我们尝试使用最先进的模型发现器（如MACE 16和SEM 17）构建β的（有限）模型，但未成功。事实上，EBAe理论产生的搜索空间太大，无法在合理的时间内处理为了为了克服这些困难，我们研究了使用CLPS工具[5]的可能性，CLPS工具是一种用于包含SSET的带原子遗传有限集理论的约束求解器。该工具已成功用于工业验证问题。由于CLPS的输入语言基于集合论构造，因此我们需要将分支β翻译回SSET中文字的合取η。一旦AM的通用集合（cf.图1中的集合PID）被手动实例化为某个有限集合，CLPS可以找到η的解（如果有的话），该解（可能）构成AM（的实例）的转换，导致违反不变量的状态。但是，请注意，我们不能保证从初始状态（由图1中的INIT子句指定）开始执行AM就可以到达这样的状态。要确定状态是否可达，有两种解决方案。首先，可以使用动画工具（例如[12]中集成的动画工具）来发现是否存在从初始状态到CLPS找到的AM的执行其次，使用模型检查器（如SMV）检查CLPS找到的状态是否可以从初始状态到达。在第二种情况下，我们应该将AM转换为模型检查器的输入语言。这应该是可能的，因为我们考虑的是原始AM的有限实例，因为我们已经将AM中的全集实例化为有限集，以便调用CLPS。一旦CLPS发现的状态的可达性被建立，反例可以被用作通过改变系统或通过加强不变量来校正初始AM的基础。例4.4（流程管理器-续）为了说明，我们考虑图3的Ready操作的（错误）规范，1 6 http：//www-unix. m cs. 安湖gov/A R/m ac e2/17http://www.cs.uiowa.edu/~hzhang/sem.html204J. - F. Couchot等/ Electronic Notes in Theoretical Computer Science 95（2004）189-208就绪=ANY-W WHERE-W ∈waitingTHEN/* waiting：= waiting-{-}||*/IF（active/=active）THEN准备好了，准备好了其他活动：结束结束图3.第三章。一个错误的操作就绪规范。必须被视为图1中AM的一部分。 在这次行动中，一名亲-已 经 等待的Cess PW以某种方式被解除阻塞，并且如果系统空闲，则可以进入就绪状态或活动状态。该bug由leav-在，在等。结果，不变量被违反，因为在下一个状态处等待和活动的交集将包含pw并且将不再为空。（请注意，要纠正这个问题，取消注释图3中由/* 和 */分隔的行就足够了。） 我们希望通过使用上述方法来检测异常情况。 首先，我们生成验证条件（沿着第2节的路线）。 然后，我们翻译并操作得到的公式，以便HARVey可以处理它（参见。第3和第4节）。 系统发现证明义务是无效的，并返回以下