抽象模型建立用于模型检测工具：αSpin

17《理论计算机科学电子札记》66卷第2期（2002）网址：http://www.elsevier.nl/locate/entcs/volume66.html16页模型检测Mar'ıadelMarGallardo，Jesu'sMart'ınezPedroMerino，Ernesto PimentelDpto.deLenguajesyCienciasdelaComputacio'nUniversityofM'alaga，29071M'alaga， Spain摘要抽象方法已经成为软件系统自动验证中最有趣的话题之一，因为它们可以减少要探索的状态空间，并允许对更复杂的系统进行模型检查。然而，缺乏真正支持这种技术的工具。 抽象系统的一个方向是将其形式化描述（模型）转换为用相同语言指定的更简单的版本，从而跳过为抽象模型构建特定（模型检查）工具。模型的抽象之后应该是要检查的时态公式的抽象。本文介绍了αSpin，它是一个将几种抽象方法（模型和公式）集成到著名的模型检查器Spin中的工具。特别是，αSpin集成了两种对偶方法，一种是基于欠近似性质的经典抽象方法，另一种是作者提出的另一种方法，其中抽象提供了公式的过近似2关键词：模型检测，抽象，工具，Spin1介绍基于计算机的验证方法，如模型检查[1]，已成为关键系统开发中使用的现实技术然而，只有当一个有用的系统模型可用时，模型检查才有成效。有用是指系统的抽象表示，只包含确保某些属性的满足（不满足）为我们提供有关系统实际行为的信息的细节描述过多细节的模型可能会产生状态爆炸问题，这可能会阻止使用当前工具对其进行全面分析。这个问题既包括符号方法，也包括显式模型检查;它们都采用抽象解释的思想[5]来构造抽象状态空间或模型[2，6，4，13]。然而，大多数实现抽象的建议都集中在2项目TIC 99 -1083-C 02 -01和TIC 2001 -2705-C 03 -02支持的工作1电邮地址：gallardo,jmcruz,pedro,ernesto@lcc.uma.es2002年由ElsevierScienceB出版。 诉 操作访问根据C CB Y-NC-N D许可证进行。GALLARDO，MART'INEZ，MERINO，PIMENTEL18关于象征性方法，对第二种方法的工具有很大的需求。本文提出了一种用抽象扩充显式模型检查器的方法。虽然我们的技术可以应用于不同的工具，但我们描述了αSpin，它是Spin [16，17]之上的实现用自动抽象扩展模型检查器应该改进Clarke等人在[2]中列举的一些经典步骤：a）定义一个适合于要验证的时间属性的抽象函数，b）构建抽象模型，c）将验证结果与原始（具体）模型的行为联系起来。关于步骤（a），我们建议使用一个抽象库，其中包含先前定义的抽象函数，这些函数可以根据要分析的属性使用[10]。这一思想也在[9]和[13]中得到应用我们构造抽象模型（b）的方法是基于模型和公式的语法转换。这允许我们重用相同的工具（Spin）来验证抽象模型。该方法还为我们提供了一个框架来推理转换的正确性，如[10]中所讨论的最后，我们将转换基于XML的使用[19]，以便尽可能独立于实际的建模语言[12]。关于结果的关系（步骤c），抽象时态逻辑的经典方法是基于定义一个抽象的可满足关系，它欠近似标准关系[2，6]。因此，它适合于检查时间公式是否对所有执行路径都为真（通用属性的satisfaction）。我们引入了一种基于时间公式过近似的新方法[11]，可以用来确保抽象模型中的任何路径都不可能满足公式（存在公式的我们的经验表明，给定一个模型，这两种双重方法都可以有效地用于核查工作。因此，我们将这两种技术集成到我们当前的实现αSpin中。此外，该实施也使我们能够探索如何从同一公式中的两种方法组合中获得更多收益其他工具也支持通过语法转换进行抽象，但它们主要面向编程语言，而不是形式化描述技术。此外，这些工具产生的抽象模型在不同的语言，从而缺乏重用的模型检查器的优点像FeaVer [18]、Bandera [9]或JPF的第一个版本[15]这样的工具被认为是Spin的抽象工具，因为它们从源代码（C，Java）中生成（提取）PROMELA我们认为α自旋是对这些工具，因为他们处理不同的问题。在模型提取中，主要的目标似乎是如何在我们的例子中，我们从一个相对简单的模型开始，我们的工作重点是逐步地将抽象应用到初始的和新的PROMELA模型。有关抽象技术和相关工具的概述，请参见[7]。GALLARDO，MART'INEZ，MERINO，PIMENTEL19||||P rocess：：=[active["[“NumberOfInstance s“]”] ] proctypeP r ocessT y pe I D { D e c l ; I nst S e q } I nst S e q：：= [ l：] I nst { ; [ l：] I nst }初始化：：= B asic|JUMP|If|Do|原子|DStepBasic：：= BExp|分配|输入|输出|RendezJump：：=gotol|打破If：：=ifBranchSeqfiDo：：= doBranchSeqod原子：：=原子Input：：=输入ID？ExpSeq输出：：=已删除 ID！ExpSeqRendez：：=输入|输出分支：：=：：InstBranch Seq：：=Branch{Branch}Fig. 1. 部分PROMELA本文的结构如下。第2节包含Spin及其输入语言的第3节和第4节分别通过PROMELA和时态逻辑的转换给出了在第5节中，我们解释了如何将αSpin与先前发表的升力控制器系统一起使用作为案例研究[8]。第6节专门介绍αSpin的实现细节。在最后一节中，我们讨论了工作的主要贡献，并概述了一些未来的工作。2PROMELA、LTL和SPIN在过去的几年里，Spin已经成为学术和工业领域最受欢迎的模型检查器之一[16，17]。它支持在用PROMELA建模语言编写的系统中验证常见的安全属性（如死锁的存在），以及分析用线性时序逻辑（LTL）表达的复杂它也被用作尝试新的强大算法来攻击状态爆炸问题的平台。2.1使用PROMELAPROMELA是一种设计用于描述由并发异步通信进程组成的系统的语言。APROMELAmodel P = Proc1. Procn由一组有限的进程、全局和局部通道以及全局和局部变量组成。进程通过消息传递进行通信-通过渠道。通信可以是异步的，使用信道作为有界缓冲器，并且可以是同步的，使用大小为零的信道。全局通道和变量确定进程运行的环境，而局部通道和变量建立进程的内部局部状态。PROMELA是一种非确定性语言，它从Dijkstra的保护命令语言、Hoare的CSP语言和C编程语言中借用了一些概念一个PROMELA过程被定义为一系列可能被标记的句子，前面是陈述部分（见图2中的例子）。PROMELA中的基本语句是那些对模型状态产生确定性结果的语句;换句话说，赋值、向（从）通道发送（接收）消息的指令以及布尔表达式BExp，其中包括对变量和内容的GALLARDO，MART'INEZ，MERINO，PIMENTEL20图二. XSpin中的升力系统模型和LTL公式的渠道。此外，PROMELA还有其他非基本句，如非确定性的If和Do句。2.2时态逻辑Spin验证了LTL公式对PROMELA模型的影响。线性时态逻辑的良构公式（LTL）是从一组原子命题（在PROMELA中，命题是对数据、通道或标签的测试）、标准布尔运算符和时态运算符（always“”，eventually“”，next“O”，until“U”）归纳构造的。对于模型状态序列ti= si→si+1→. . .每个序列表示从状态s i开始的一个可能的模型执行。使用时间操作-ators允许构造依赖于配置序列当前和未来状态的公式LTL的语义如图3所示，其中p是一个命题，f和g是时间公式。为了方便起见，我们假设所有公式都是否定范式，即否定只出现在命题中。请注意，我们没有包括一个规则来定义否定公式的满足。相反，我们对待否定命题的评价一个。其原因将在第4节中解释图中的最后两个规则3定义了泛时间公式和存在时间公式的语义在这里，M表示模型产生的执行轨迹集。2.3自旋默认情况下，给定一个LTL公式，Spin会将其转换为表示不希望的行为（声称这是不可能的）的自动机。然后，验证由状态空间搜索的详尽探索组成GALLARDO，MART'INEZ，MERINO，PIMENTEL21我不是|=pisi|=p我不是|=100fij≥i.tj|=fti|=fij≥i.tj|=f ti|=Ofi ti+1|= f我 不 是 |=fUgik≥i. 你 好 i≤jMiddle：(((x==Middle））->noLower：(((x==noUpper））->noLower：(((x==noLower））->noLower：(((x==Unknown））->noLower：（ILLEGAL）在这段代码中，使用常量ILLEGAL来表示。图2中的代码现在被下面的代码所取代，它说明了使用抽象指令（e_e_ect_α）来增加变量Position[]。public int findDuplicate（int findDuplicate）{做...：：SysLift_Lift[pid]？命令;如果：：（Order==Up）-> FLR_INCR（Position[pid]）;...}采用相同的方法来实现测试α。例如下一定义包含FLR EQ的实现（（i==j）的抽象测试#defineFLR_EQs（x，y）（（x==Lower &&y==Lower）||（x==上限&&y==上限））#defineFLR_EQw（x，y）（x==Upper）&&（y==noLower））||（（x==无下限）&&（y==上限））||((x==下限）&&（y==noUpper））||（（x==noUpper）&&（y==Lower））||（（x==中间）&&（y==noUpper））||（（x==noUpper）&&（y==Middle））||（（x==Middle）&&（y==noLower））||（（x==noLower）&&（y==Middle））||（（x==未知））||（（y==未知））#defineFLR_EQ（x，y）（FLR_EQw（x，y））||FLR_EQs（x，y））函数FLR EQ验证了抽象模型正确模拟原始模型所需的正确性条件（在[10]中研究）。非正式地说，当a==b对于分别由x和y抽象的一些具体数据a和b成立时，FLR EQ（x，y）为真，如（Over）等式中所定义的这解释了为什么FLR EQ（Upper，noLower）返回true。下面将解释使用两个宏（FLR EQ和FLR EQw）定义FLR EQ的原因用户必须选择要抽象的变量和要应用的抽象（α），然后自动执行转换4抽象时态逻辑一旦模型使用上一节中描述的方法被约简，接下来的步骤是定义时间公式对抽象模型的满意度（称为抽象满意度），并将其与公式对原始模型的满意度关于PROMELA模型的LTL公式中的原子命题是布尔表达式。因此，考虑图3中给出的满足性的标准概念，并遵循用于抽象模型的相同思想，我们可以断言，为了定义时间公式GALLARDO，MART'INEZ，MERINO，PIMENTEL25CCCCCCCCCCCC它表面上是为了定义原子命题的抽象满足一个明显的可能性是使用函数testα，如前一节（Over）所定义的，来评估原子命题。使用检验α，我们构造了抽象时态公式的所谓过近似方法，在[11]中已经详细研究过另一种可能性是使用下面的函数测试α来评估原子命题。给定p∈BExp和sα∈Stateα，测试α定义为检验α（p，sα）={s∈状态.α（s）≤αsα}测试（p，s）（低于）结合模型检验和抽象的经典论文[2，6]使用函数测试α来评估时态公式。函数测试α结合了在某些情况下可能会感兴趣的对偶方法，如下一节所讨论的。现在，我们总结的主要理论结果之间的关系，抽象模型（使用经典和过近似的方法）和具体模型的满意度的时间公式的抽象满意度在本节的其余部分，我们写道：(i) S|= p当test（p，s）成立时，(ii) sα|当检验α（p，sα）成立时，= α p，并且(iii) sα|当检验α（p，sα）成立时，= α p。我们还要|=，|= α和|= α抽象的痕迹定义的意义时间操作符如图1所示3. 请注意，例如，当我们写Mα|=α<$f，我们有一个条件是α∈G（M，e ∈ctα，testα）. tα|=αf，等等。下面的定理给出了前面定义的两个直接结果在定理中，我们假设G（M，e，t，α）是模型G（M，e，t，α）的正确过逼近，并且原模型是无死锁的.定理4.1给定时间公式fMα|=αfM|=ΔfM α|=αf M |= 100f第一个结果对应于经典的弱保存universe-在[6]中研究了盐的性质利用经典方法论，从抽象到具体模型，直接保持了对泛属性的第二个结果是双重保存结果。使用过近似方法，存在性的反驳直接从抽象到具体的模型。请注意，这些结果是不等价的，因为它们使用非标准和对偶方法处理否定 给定一个命题p和一个抽象状态sα，使用def-初始化（Under），对于经典方法，检验α（p，sα）和检验α（<$p，sα）都可能不成立。而在《易经》中，则是以“卦”为卦。GALLARDO，MART'INEZ，MERINO，PIMENTEL26¬CCC近似方法，检验α（p，sα）和检验α（p，sα）都成立。这就是为什么我们跳过图3中的否定规则。因此，考虑到对于mula<$f是否定范式，我们有Mα|=αf/Mα|=α<$f，此外，Mα|=αf/Mα|=αf。4.1LTL的句法转换在前面讨论的基础上，时态公式的句法转换是直接的第一步是将公式写成负正规形式（如有必要）。然后命题被自动替换为测试的抽象实现，这取决于所采用的方法。对于过近似方法的实现，使用所采用的测试α的相同定义来定义命题to transform变换the model模型. 但是测试α的实施一定要更重--比试验α更严格，以确保上述（下）定义的标准一个类似于#define FLR_EQs（x，y）（（x==Lower&& y==Lower）||（x==上限&&y==上限））实现（i==j）的（经典）抽象测试。非正式地，当a==b分别对x和y抽象的每个具体数据a和b成立时，FLR EQs（x，y）为真，如（Under）中所定义的。注意，FLR EQ使用两个宏FLR EQ和FLR EQw，以便考虑仅一些具体状态满足（i==j）的情况5使用αSpin：案例研究在本节中，我们将介绍αSpin为Spin/XSpin添加的主要功能。我们的案例研究是[8]中介绍的电梯控制器的PROMELA在本节中，我们将展示如何使用对偶方法来反驳和验证时间属性。第一个实验是通过反驳（用过近似法）来消除错误。第二种方法是用经典的方法检验所需的泛性质。5.1模型最初的规范考虑了一个控制器系统来管理n台电梯，我们的目标是验证相同的控制结构也只适用于一台电梯。按照如何构建合适的模型进行验证的规则，我们已经做了一系列的修改，以使用一个电梯（见图11）。5）。系统的输入由一个过程建模，该过程从电梯内部产生用户请求升降机用Lift（）进程表示，它接收向上、向下和停止的命令，从而更新每个命令的位置控制部分接收输入并将命令发送到Lift（）进程。这部分分为几个进程（SysLift（），GALLARDO，MART'INEZ，MERINO，PIMENTEL27Lift（）nb_floor-1..320位置[ ]Internal_request[]...............SysLift（）SysStop（）采样器（）...............全局变量图五. a）升力系统示意图b）α自旋SysStop（）和Sampler（）），它们通过集合通道和全局变量进行通信。在每个过程中控制升降机的主要变量是全局变量Position，它始终存储升降机的当前升降机全局数组internal request[nb floor]存储移动到特定内存库的挂起请求，nb floor是系统中内存库的实际数量。图中的代码图2显示了在Lift（）过程中根据来自控制部分的命令（Up、Down、Stop）更新此变量。5.2丢弃错误检查控制系统是否正常工作的一个关键属性是在没有请求的情况下没有移动。NoMove属性表示如果我们想检查电梯在下楼梯时的属性，我们可以将其编码为时间公式NoMove：>（posL no_request> possiveL）然后我们可以使用Spin来验证没有满足公式的执行（在图中完成）。2），其中命题posL和possiveL表示电梯当前是否在较低楼层上或上方，并且没有请求表示电梯没有用户。这些命题是根据它们的解释标准或抽象定义的，如第4节所述验证具体模型（具有命题的标准含义）的主要问题是，验证时间高度依赖于模型的数量，并且当该参数增加到高值时，它是不可扩展的。幸运的是，公式NoMove中的命题给了我们如何抽象的指导。由于对这些命题的评价主要是GALLARDO，MART'INEZ，MERINO，PIMENTEL28依赖于变量Position[]的值，此变量用于作为计数器，我们可以使用FLOORS抽象来减少要访问的状态空间。然而，FLOORS的使用意味着全局数组内部请求[nb floor]必须由只有三个组件的数组抽象。抽象工具通过分析模型的结构来建议这些信息，用户也可以从图5所示的输出中猜测这些信息。GUI给出了关于模型中包含的变量的信息（名称，类型和上下文：全局或局部），抽象库中适用于时态公式中变量的可用模板以及变量与抽象函数的当前绑定（位置[1]将使用FLR进行抽象）。当选择了抽象函数后，αSpin根据用户的选择执行模型的语法转换。如图6所示，当选择Propertiesholds for No Executions（错误行为）时，代码将采用公式的过度近似。宏FLR EQ、FLR GT、FLR NE、.. 如前所述，实现这种过度近似，测试α。如图6所示，这个误差既不存在于抽象模型中，也不存在于具体模型中（使用定理4.1）使用抽象公式来排除这一错误的好处在图中作了总结8.第八条。用于检查运动的公式是前一个公式的扩展，也考虑了上、中跨舱的偏离与具体模型相比，访问状态的预期数量大大减少（见图2）。8）。此外，状态数的变化相对于门的数量是线性5.3验证所需行为在丢弃关键的关键错误行为之后，我们继续验证电梯系统是否能够提供预期的服务。该物业移动说，作为期望行为的属性的版本可以如下：移动：[]（（reqL posU）->> posBelowU）（（reqU posL）-><> possiveL）（（reqM noPosM）->> posM））其中，命题reqL、reqU和reqM分别表示来自Lower、Upper和Middle缓存的请求命题posU、posBelowU、posL、possaveL和noPosM表示电梯当前是在特定楼层之上还是之下。同样，这些命题是根据解释标准或非标准来定义的，这取决于如何进行验证（具体或抽象模型）。模型的转换（自动）方式与反驳情况相同，但当选择所有执行的属性（期望行为）时，公式转换（自动）为采用经典方法。请注意，在图7中，公式中的命题是使用宏FLR EQ、FLR GT、FLR NE.. 实现了经典的GALLARDO，MART'INEZ，MERINO，PIMENTEL29C见图6。 对错误行为见图7。 验证预期行为欠近似检验α现在，抽象公式中的验证结果用这种方法验证的好处如图所示8.第八条。6执行在我们的抽象工具的主要设计标准是获得尽可能多的独立性与特定的建模语言和模型检查器因此，我们将XML视为唯一的内部表示，以通过转换执行抽象，如图9所示。实际的建模语言可以通过前端模块翻译成这种表示（图1中的步骤1和29）和模型检查器的最终抽象模型可以由特定的后端模块生成（步骤6和7）。此外，如果我们对模型和抽象函数使用相同的内部符号，我们可以集中精力开发可重用的技术和基于转换的抽象的统一工具。除了使用浏览器和其他用户友好的表示工具等实际原因外，面向XML受到许多更多技术原因的支持（参见[12]）。由于每个模型检查器都使用特定的输入，从建模语言的角度来看，每个模型检查器都有一个特定的解析器和额外的支持来转换模型GALLARDO，MART'INEZ，MERINO，PIMENTEL30见图8。 验证结果具体化为模型检查阶段的适当内部数据结构。不幸的是，访问这种内部表示并不是一种常见的做法，因为模型检查工具是源代码封闭的，或者不足以通过一组API实现数据转换或操作，如抽象所需即使在像Spin这样的开源项目中，执行抽象的大部分工作也不能直接重用于其他模型检查器。 此外，模型的XML简化了抽象工具中的传统任务，例如查找关系在变量之间或定位使用特定变量的点。关于抽象函数，XML是表示具体和抽象数据以及抽象操作之间的映射的强大手段，包括诸如操作数类型、关联规则等细节（见图11）。10）。此外，整个抽象库可以定义为XML仓库。当前的实现由图1所示的模块组成9.第九条。它们中的大多数已经完成，我们现在正在开发抽象证明器，它将帮助生成新的正确的抽象函数，并将其包含在库中。7总结发言本文的主要贡献是提出了一种在显式模型检测的背景下通过语法转换进行抽象的工具。我们已经介绍了α Spin的实际状态，这是一个集成了经典抽象方法和我们的过近似方法的工具。α Spin的文档以及当前和未来版本可以在[20]中找到。支持转换的理论方法为我们提供了一个安全的框架来扩展实现，保留了抽象和具体模型（和公式）中的结果之间的关系例如，我们已经实现了一个方法来检查存在性属性（那些至少对一个路径为真的要做到这一点，模型必须被转换GALLARDO，MART'INEZ，MERINO，PIMENTEL31C图9.第九条。基于XML的抽象体系结构和αSpin的模块见图10。 XML基础抽象库使用最受约束的抽象检验和测试版本（检验α和测试α），并使用测试α转换公式。我们现正扩展C c理论框架，以支持新的转变（相关工作可以在[4]中找到其他有趣的贡献是使用抽象库和使用XML来支持抽象过程。该库应用于存储在验证经验中显示为有用的新函数甚至可以给这些函数一个分类法，使它们的使用更容易[14]。同样，XML是存储这些信息的一个很好的选择我们未来的工作是增加策略，以自动分析的正确性，抽象功能使用PVS。另一项工作是改善反例分析[3]。鸣谢我们要感谢推荐人的有益和建设性的意见。引用[1] E.M. Clarke，E. A. Emerson和A.P. Sistla使用时态逻辑规范自动验证时态并发系统，ACM TOPLAS，8（2），（1986）。GALLARDO，MART'INEZ，MERINO，PIMENTEL32[2] E.M. Clarke ， O. Grumberg 和 D.E. 久 了 Model Checking and Abstraction ， ACMTOPLAS，16（5），（1994），1512[3] E.M. Clarke，O. Grumberg，S. Jha，Y. Lu和H.维斯反例引导的抽象细化，Proc. ofthe 12 th CAV，LNCS-1855，pp. 154-169，（2000）.[4] R. Cleaveland ， S.P. Iyer 和 D. 扬 克 列 维 奇 模 型 检 验 中 的 最 优 性 与 抽 象 。 以 .Mycroft，编辑，静态分析研讨会，LNCS-983，pp.第51-63条，（1995年）[5] P. Cousot 和 R. 库 索 Abstract Interpretation ： A Unified Lattice Model for StaticAnalysisof Programs by Construction or Approximation of Fixpoints. 第四届ACMSymp.关于POPL，pp. 238-252，（1977）。[6] D. 达姆斯河Gerth和O.Grumberg. 反应系统的抽象解释ACM TOPLAS，19（2），（1997），253[7] D.水坝。软件模型检查中的抽象：原理与实践，第9届国际SPIN研讨会。 模型检查软件，LNCS-2318，pp. 2002年14-21日[8] G. Duval和T.卡特尔从架构到安全过程控制应用的实施。设计、验证和模拟。在第13届夏威夷国际年会上，Conf. 《系统科学》（1997年，第30期）。[9] M. Dwyer，J.Hatterdham，R. Joehanes，S.劳巴赫角帕萨罗湾Visser，H.郑工具支持的程序抽象用于验证状态。 Proc. 2001年，ICSE。[10] M.M. Gallardo和P. Merino。一个自动构造抽象PROMELA模型的框架。在自旋模型检验的理论和实践方面，LNCS- 1680，pp。184-199，（1999）.[11] M.M. Gallardo、P.Merino和E.皮门特尔并发系统的抽象LTL性质。第六届世界集成设计&过程技术大会（2002年）的报告。出现。[12] M.M. Gallardo，J.Martinez，P. Merino和E. Rosales，使用XML实现模型检查的抽象。ACM Symposium on Applied Computing，pp. 1021-1025（2002）。[13] S. 格拉夫使用抽象验证分布式缓存在迪尔，（编辑）计算机辅助验证，LNCS-818，pp。207-219，（1994）。[14] S.格拉夫个人沟通。2002年。[15] Havelund K.，Pressburger T.使用Java Path对Java程序进行模型检查Software Tools for Technology Transfer（STTT）2（4）：366-381，（2000）.[16] G.J. Holzmann Comp.方案的设计和验证。Prent-Hall，（1991）.[17] G.J. 霍尔茨曼模型旋转。 IEEE Trans. 关于SE，23（5），（1997）。[18] G. J. Holzmann和M. H.史密斯事件驱动系统验证的一种实用方法。 在proc 第99章，pp. 597-608，（1999）。[19] W3财团。可扩展标记语言（XML）1.0（第二版），可在http://www.w3.org/XML/（2000）中获得。[20] α自旋项目 马拉加大学。www.lcc.uma.es/网站地图