VHDL状态机的模型检测与CTL性质验证方法

1理论计算机科学电子笔记66第二次（2002年）网址：http://www.elsevier.nl/locate/entcs/volume66.html16页模型检测VHDL状态机穆斯塔法·布拉赫拉计算机科学系，比斯克拉大学BP 145 RP，Biskra，阿尔及利亚，07000电子邮件地址：mbourahla@hotmail.com穆罕默德·本·穆罕默德康斯坦丁大学计算机科学系，阿尔及利亚，25000摘要本文提出了一种抽象-精化的自动组合方法，将描述状态系统的VHDL模型转换为SMV描述的初始等价抽象系统，探索其状态空间，验证CTL的性质。我们提出的方法实现自动计算抽象决策过程。这种方法可以处理不同类型的无限状态系统，包括由并发组件组成的系统，它可以扩展到更复杂的VHDL概念。抽象模型可能会允许虚假的反例（假阴性结果），这些反例是在抽象级别上执行的，而在具体级别上没有相应的执行。我们设计了一个新的算法，分析这样的反例，并通过逐步消除假阴性结果相应地细化抽象模型 我们用一个例子来说明我们的方法，并在一个大型设计中证实其有效性1介绍数字系统的抽象解释的主要思想是在一个不同的抽象（因此简化）系统中解释系统的行为，该系统具有较少的状态，用于处理将模型检查应用于大型工业设计时的状态爆炸问题。抽象可以被看作是两个系统之间的关系。一方面，原始系统具有其行为的完整描述，而其抽象保留了一些行为并抽象了其余部分。然后在抽象系统中执行验证任务。 有两种类型的抽象：精确抽象是那些在抽象系统中验证的结果意味着2002年由ElsevierScienceB出版。 诉 操作访问根据C CB Y-NC-N D许可证进行。BOURAHLA和 BENMOHAMED2在具体的系统中，效果相当。另一方面，在保守抽象的情况下，只有抽象系统的验证中的某些结果才能隐含在原始系统中。抽象验证似乎很有希望用于推理控制密集型设计，其中控制是有限的，但数据部分是有限的或非常大[9][10]。抽象模型通常是手动提供的，而- orem证明用于检查所提供的抽象映射是否保留了属性。最近，基于抽象解释的新技术已经被提出，在时间属性的验证的上下文中，定理证明被用于自动计算有限抽象[2][7] [8]。这些技术是相当有效的，但需要大量使用理论证明和决策过程。有一些方法/工具可以从有限状态程序的文本和抽象关系中计算抽象系统[6]。应该认识到，在生成抽象系统之前，避免对表示所考虑的程序的语义的具体模型的描述是很重要的。否则，将不得不存储可能太大的具体系统。生成的抽象系统通常比具体系统小，因此模型检查要简单得多。抽象验证也可以应用于无限状态系统，如[12]所示。然而，在所有这些方法中，验证者必须提供抽象系统，并且需要大量的用户干预来证明抽象系统模拟了具体系统。 所需要的是一种自动计算给定无限状态系统和抽象关系的抽象系统的方法。实现这一点的方法，[14]中给出了抽象函数的一种限制形式，即由具体状态上的一组谓词引起的抽象函数。然而，这种方法的缺点是，它生成一个抽象的图形，而不是一个抽象程序的文本，其结果是，既不能应用进一步的抽象，也不能应用避免状态爆炸问题的技术，例如，偏序技术。在抽象系统的构造过程中，还有另一种基于消除的方法[3]。然后，为了从将每个抽象状态与每个抽象状态相关联的泛关系出发构造具体转换的抽象转换，该方法消除抽象状态对，使得在消除一对之后，所获得的转换仍然是具体转换的抽象。这种方法太复杂了，因为泛关系的转换数量是变量数量的指数。这种方法与其他基于分区的抽象变量集的技术相结合，使用subjunctions，但这种分区导致一个更不确定的抽象系统，然后更多的虚假反例。使用抽象和模型检查作为验证和分析技术的缺点在于，抽象是原始系统的近似，会导致假阴性结果。为BOURAHLA和 BENMOHAMED3例如，模型检查器可以展示对应于违反期望属性的抽象程序的执行的错误跟踪。然而，这个错误跟踪可能并不对应于具体程序中的执行跟踪.这种情况表明抽象过于粗糙，对抽象系统进行模型检验的结果不具有决定性。这是太多的细节被抽象和抽象需要细化。我们提出了一种方法，用于自动构造从VHDL模型中提取的谓词抽象，以抽象无限变迁系统，从而使抽象模型通过构造来模拟具体系统。这些系统可以由并发组件组成。但是构造抽象系统的过程并不取决于计算模型是同步的还是异步的，即，基于交织。一般来说，我们的技术计算原始系统的上近似。因此，当一个规范在抽象模型中为真时，它在具体设计中也将为真。然而，如果在抽象模型中的具体化是假的，则反例可能是近似中的某些行为的结果，而这些行为在原始模型中并不存在。当这种情况发生时，有必要对抽象进行细化。我们的方法不同于[3]中的方法，因此只消除了引起伪反例的最后一个行为。克拉克[6]他在另一个基于具体模型抽象的抽象框架中提出了其他技术，但是当存在虚假反例时，为了得到一个精化的抽象模型，他的方法通过与具体模型的行为进行比较来消除虚假反例中所有不可达的状态。这也需要时间，而且没有必要。VHDL模型是使用语言的子集[19]和从大多数综合工具中提取的某种建模风格编写的。VHDL模型状态用符号表示，抽象状态是这些状态之一与抽象布尔变量的真值赋值的结合。 假阴性结果将通过一个称为细化的自动过程逐渐消除，该过程使用从虚假反例中获得的信息验证方法基于抽象，然后是模型检查和细化。如果没有可能的细化，系统将通过将跟踪中的每个步骤映射到具体域来报告反例。我们用一个例子来说明我们的方法，实现自动构造的抽象系统。第二部分介绍了用VHDL语言对变迁系统进行建模的方法。在第3节中，我们提出了第4节中提出的抽象算法所使用的谓词抽象框架。第5节介绍了细化算法。工具概述和结果分析见第6节。最后给出了结论。BOURAHLA和 BENMOHAMED42用VHDL语言硬件描述语言（HDL），最著名的是VHDL，在硬件设计的规范中获得了相当大的普及。VHDL支持进程级并行.它采用具有复杂语义的构造来实现进程之间的并发、通信和同步[19]。VHDL结构，如信号分配语句和等待语句促进确定性进程间的通信和协调。人们可以利用VHDL的这些特性来编写简洁的行为描述。定义2.1（过渡系统）。转换系统M是元组M=（S，V，T，I），其中• S是一组系统状态• V是一组任意类型的• T是一组系统转换，每个转换与集合V上的一个防护表达式和一组动作表达式相• I是一组初始状态VHDL是一种特别适合描述过渡系统的语言，因为它的高级语法（指令，如果...然后...否则，案件...when），其允许直接翻译传统的图形表示，如图形和图表。使用VHDL语法，我们可以命名状态，信号等，这给了我们一个清晰可读的描述。为了抽象，我们选择了VHDL的一个子集来描述转换系统。转换系统可以由一个行为组件或多个并发组件组成。每个组件由一个过程描述转换系统的变量这些国家都是象征性的。引入了一个指令来编写CTL公式，以便在VHDL模型上进行检查。我们在计算两个自然数x和y的GCD（大公除数）的著名算法上说明了我们的验证方法。转换的形式是条件/动作，这意味着如果条件为真，则发生转换，然后执行动作。GCD的VHDL模型<实体GCD是port（int： in bit; x，y：ininteger; start：inout bit; z： outinteger）;终端实体GCD;GCD的体系结构行为是类型状态是（S 0，S1，S2）;信号S：状态：= S 0;信号xp，yp： 自然;开始进程开始等待直到Clk=BOURAHLA和 BENMOHAMED5--当S0 =>if start=如果start=如果xpyp，则yp= yp-xp;S= S1;结束如果;如果xp>yp，则xp= xp-yp;S= S1;结束如果;如果xp=yp，则Z= xp;S= S2;结束如果;<当S2 =>Start=结束过程;--$ AG（Start =Fig. 1. GCD的VHDL模型及其特性说明3谓词抽象谓词抽象包括在具体变量上使用谓词作为布尔抽象变量[14]。它可以在抽象解释的框架中使用伽罗瓦连接来定义。定义3.1（伽罗瓦连接的令Sc和Sa分别表示具体和抽象状态域。从Sc到Sa的伽罗瓦联络[2]是一对函数α：2Sc→ 2Sa和γ：2Sa→ 2Sc使得：• α和γ是完全单调的。• <$X∈2Sc，γoα（X） <$X，且• <$X ∈ 2Sa，αoγ（X）<$X.定理3.2（连接和模拟之间的关系）。 设Rc和Ra分别表示Mc和Ma的转移关系.若（α，γ）是Sc与Sa之间的联络，且<$SJ∈2Sa，则α（Pre（ Rc，γ（ SJ）<$Pre（Ra，SJ）则Mc≤ Ma，其中Pre是前象函数.如果P是具体变量上的谓词，则谓词抽象可以表示为Galois连接[14]如下：α（PB a|P<$γ（B）}= P a，）={ a其中B a是集合{B1，.， B k}，它是对应于具体谓词φ1，.，φ k。γ被定义为一个替换函数，即γ（Pa）= Pa [φ1/B1，.，φ k/B k]，其中每个布尔变量B i由其对应的正确谓词φ i替换。因此，抽象的一组具体的状态表示由具体变量上的谓词P定义为抽象变量Bi上的最小布尔公式Pa，即，P.用于计算关于集合的最精确的布尔抽象BOURAHLA和 BENMOHAMED6⇒⇒不我对于谓词的转移关系为关系谓词的系统，应指定一个有效的布尔组合Ba的枚举来检验断言P γ（Ba）。 这将抽象系统，转移关系作为谓词给出。 每个蕴涵P γ（Ba）提交决策程序以检验其有效性。请注意，Pa的任何近似都是P的有效抽象.因此，为了计算一个具体系统M，一个抽象系统Ma，通过计算α（I）来抽象初始状态I是足够的，并且抽象每个转移t∈T如下：t a= α（t）= α（action（V，VJ））={（B a，B aJ）|<$post [t]（γ（B a））<$γ（B aJ）}，即对（B a，B aJ），其特征在于由t对可能的前驱集合的抽象和由t，其中post通过a的转换t表示最强的post条件谓词P在V的状态变量上，定义如下：post[t]（P）=<$VJ.actiont（VJ，V）<$P（VJ），其中动作t（VJ，V）被定义为当前状态和下一状态之间的关系，即表达式：（s=si）安全防护罩Li=1（vJei）（next（s）=sj）时态逻辑中表达的属性的保持是通过具体和抽象模型之间的等价和前序来定理3.3（弱保存）。设M是一个具体系统，Ma是M的一个谓词抽象，使用任意谓词集。 我们有M A|=α（φ）M| = φ，对于每个时间公式φ。证据M的所有执行都是Ma的执行，那么如果一个属性在Ma的所有执行路径上都成立，那么它在M的所有执行路径上都成立。这意味着Ma模拟M，因为以下对于M的每个转变t成立：P.post [t]（P）✷这个定理表明，当一个属性是建立在ab-具体系统具有相应的具体属性。然而，当财产在抽象体系中不成立时，什么都不能得出结论。在某些条件下，强保持结果可以应用于这种情况。定理3.4（强保存）。设M是一个具体系统，设Ma是M的一个谓词抽象，它使用的谓词集合包括M的守卫和性质φ中出现的所有文字 如果M a是确定性的，|= α（φ）惠M |= φ，Ma和M是等价的。你可以在[14]中找到它的证明强大的保存效果让我们BOURAHLA和 BENMOHAMED7¬通过将抽象的错误跟踪映射到违反该属性的具体执行来避免假阴性结果。然而，强保存的条件要求Ma是确定性的。通常情况并非如此。每个抽象状态是布尔变量集合的一个子集的合取，这些布尔变量是有限抽象域的代码。抽象状态的具体化是一组可以表示为谓词的具体状态。我们已经使用这些谓词抽象的概念来自动抽象用VHDL描述的转换系统。下一节给出了GCD的算法和示例4谓词抽象该算法使用决策过程的谓词抽象的一个具体的，无限状态系统描述为一个transi- tion系统与VHDL的自动构造。具体系统的抽象M=（S，V，T={t1，...， t n}，I）是一个抽象系统Ma=（S，Va，Ta={ta，...， t a}，I a）这样1N认为：•Va是集合{B1，...， B k}• Ta是一组抽象的转换。• Ia是抽象的初始状态，计算为α（I）。抽象算法包括计算Ia，并且对于定义为（s=si）的每个具体转换t，对应的抽象转换ta定义为（s=si）的每个具体转换t，对应的抽象转换ta定义为（s = s i）的每个具体转换t，对应的抽象转换ta定义为（s=si）的每个具体转换t，算法1抽象步骤1：使用转换保护中的谓词和CTL公式定义抽象函数α。函数γ是相应的替换函数。步骤2：对于每个保护，抽象保护（保护a）计算为α（保护）。当使用守卫的字面量作为抽象布尔变量时，α（守卫）是一个精确抽象，其中守卫的每个字面量在语法上被其对应的抽象布尔变量替换。步骤3： 构造所有布尔表达式Ba的列表L，（B i/ B i）使用抽象变量。第四步：每个转换的动作分配将被抽象为由最大数量的抽象变量组成的布尔表达式，它应该验证含义：post [t]（true）<$γ（抽象布尔表达式）。“抽象布尔表达式”是所有布尔表达式的合取B a取自列表L，其中蕴涵post [t]（true）<$γ（B a）是有效的。 这意味着，对于这个表达式中的每个抽象变量B i，任意状态的最强后置条件是在γ（B i）或在<$γ（B i）中，即在φi或在<$φ i中。如果抽象变量不在表达式中，这意味着它不是确定性的。步骤5：变量S没有被抽象，因为它是有限类型的。BOURAHLA和 BENMOHAMED8}↔- 参与者}{4.1关于示例我们使用的谓词从VHDL模型中提取的具体变量在解析VHDL模型（图1）后生成的转换表如表1所示N现状警卫队行动下一状态守着一动作a1S0开始= 0空S0B1空2S0开始= 1xp：= x; yp：=yS1€B1空3S1XP YP ypxp：= xp -ypS1B3空5S1xp = ypz：= xpS2<$B2<$B3空6S2真开始：= 0S0真B1：=true表1 GCD列Guarda和Actiona在抽象之后填充首先，我们计算抽象的初始状态。VHDL模型包含一个初始化语句（S：=S 0），这将不会被抽象.抽象初态是满足公式（S=S0）的任意状态.其次，我们计算所有转换的抽象守卫以及指定谓词。列Guard中显示的谓词集与从指令显示的CTL公式生成的谓词--$（在这种情况下，集合是{Start=J 1J，xp=yp），将是到抽象算法，用于使用决策过程产生抽象布尔变量的集合和每个具体谓词的等价抽象谓词。该算法将逐个获取Guard列中的谓词，并尝试用已经构造的抽象变量来表示它们。如果不可能，它将谓词分解为更简单的pred- icates（通过更简单，我们的意思是删除布尔连接器），然后，它将一个新的抽象变量关联到其中一个尚未关联的变量，然后它将重试该过程，直到谓词完全用构造的抽象变量表示。我们将重复这个过程，直到所有谓词都可以用抽象变量表示如果我们例子中的抽象变量集是B1 for（start= 0），B2 for（xpyp），B3 for（xp > yp），这意味着抽象函数α是由谓词（B1（start=0））（B2（xp yp））（B3（xp > yp））定义的，那么我们需要使用对决策过程的调用来用最少的抽象变量来表示所有的守护谓词。例如，转换数3的抽象保护（见表1）是B3，因为蕴涵（（xp=yp）B 3））被检查为有效。第三，我们计算每个转移动作中每个赋值的抽象。分配位于“操作”列中。我们需要实现抽象变量的最大数量（或其BOURAHLA和 BENMOHAMED9⇒其中一个PS∧∧∧否定）来抽象这些赋值，使得下面的含义布尔抽象变量）”应该是有效的。这些含义将通过调用决策过程来检验。一个动作的抽象是它的分配的所有抽象的结合。在构造完所有抽象谓词之后，翻译程序将生成等价的SMV模块（图2）。SMV系统[20]是一种用于根据时序逻辑CTL中的规范检查有限状态系统模块主VARB1：boolean; B2：boolean; B3：boolean; S：{S0，S1，S2};INITS = S0TRANS（S = S0& B1&next（S）= S0）|（S = S0&！B1&next（S）=S1）|（S = S1& B2&next（S）= S1）|（S = S1& B3&next（S）= S1）|（S = S1&！B2&！B3&next（S）= S2）|（S = S2next（B1）next（S）= S0）INVAR（B2&！B3）|（啊！B2&B3）|（啊！B2&！B3）规格AG（！B1 -> AF（！B2&！B3））图二. 抽象模型4.2不变量生成在SMV模块（图2）中，有一个不变量。不变量是一个表示状态集合的公式，系统中每个可达的状态都在这个集合中。不变公式是为了使已经生成的抽象布尔变量之间保持一致，从而不会得到一个没有意义的公式的状态，从而避免系统到达无用的状态。举例来说，不会有任何具体的状态验证公式B2B3（它在具体域中的等价物是下面的算法的思想是检查（B2B3）是否是重言式.如果是，该组合将从不变公式中删除算法2不变量生成考虑B是抽象布尔变量的集合考虑P是等价谓词考虑PS是来自P的子集的集合，其中来自PS的每个元素的谓词使用具体变量考虑BS是来自B的子集的集合，其中每个Bj∈B是我BOURAHLA和 BENMOHAMED10←J←∧<$B1<$B 2<$$> B3<$（S=S 0）<$B1<$B 2<$B3<$（S=S 1）不变真对于每个BS，如果BS包含一个以上的元素，J J对于（BS中所有Bj或非Bj的每个合取C），如果不是有效的（不是γ（C）），则不变不变 C如果结束，则结束端该算法首先搜索抽象布尔变量，这些抽象布尔变量是使用相同的具体变量的具体谓词的抽象，并将它们分组在变量簇中。然后，算法将尝试检查由这些变量集群组成的所有合取。如果等价连词在具体域中的否定被检查为重言式，它将不会被插入不变式中。我们应该注意到不变量可以为真（空）。4.3抽象模型一旦一个抽象系统被构造，SMV模型检测系统被用来探索其状态空间。模型检验相对于其他验证技术的优势在于，当一个属性被违反时，它能够生成反例。错误跟踪是从系统的初始状态开始的一系列状态和转换，导致违反属性的状态。抽象系统的错误跟踪可以映射到具体系统的执行，因为每个抽象转换对应于单个具体转换。图3显示了一个错误跟踪，它是一个破坏指定属性的假循环计数器示例。图三. 误差轨迹在具体系统上的错误跟踪的模拟表明，它不对应于具体系统的执行。但这并不排除财产被侵犯的可能性。在下一节中，我们将提出一个算法来展示模型检查如何指导抽象系统的自动细化，直到属性被验证或生成对应于违反属性的具体执行的反例。5抽象的自动细化上面的具体化并不满足于已经构建的初始抽象系统。系统SMV生成了一个错误跟踪，指示违规BOURAHLA和 BENMOHAMED11∧∧∧此规格（图3）。通过对这个错误跟踪的分析，我们了解到抽象系统正在执行一个在具体制度。抽象的体系太抽象了，需要细化。换句话说，转换数4（见表1）由公式（S=S1）定义B3next（S）=S1）。布尔变量B3可以得到下一个值真或假，这不是确定性的，但在具体的系统中，下一个值（xp > yp）最终将得到值假。图4显示了在该模块的细化过程中的每个步骤之后生成的不同反例（A，B和C），直到满足特定的活性属性。BCAG（！B1−> AF（！B2！B3））是真图四、通过模型检查不同级别的细化生成的错误跟踪因此，我们已经对从初始抽象模型（图2）逐渐细化产生的四个抽象模型进行了模型检查，直到验证了属性。在下文中，在介绍我们的精化算法之前，我们将解释我们在这个例子中的精化方法我们采用错误跟踪中最后一个转换te的公式（参见图3）te（S=S1）<$<$B1<$$>B 2<$B 3<$$>下一个（B1）<$$>下一个（B2）<$下一个（B3）<$（下一个（S）=S 1）通过映射到我们已经拥有的抽象转换系统（初始抽象模型），等价的抽象转换ta是（参见图2）ta（S=S 1）B3（next（S）=S 1）这个转换公式应该验证要考虑的等式te ta=te。在我们的方法中，我们只取抽象谓词中使用的抽象变量，谓词由转换tc的动作使用的具体变量组成，转换tc以t作为其抽象转换（在这种情况下，B2和B3）。 然后，我们取一个抽象变量（例如，B3）。 谓词next（B3）在te中（因为，tenext（B3）=te），而不在ta中，因为tanext（B3）/=ta。那么我们应该检查<$B1<$B 2<$$> B3<$（S=S 0）一<$B1<$B 2<$$> B3<$（S=S 0）<$B1<$B 2<$B3<$（S=S 1）<$B1<$B 2<$$> B3<$（S=S 1）<$B1<$B 2<$$> B3<$（S=S 1）<$B1<$B 2<$$> B 3<$（S=S0）<$B1<$B 2<$$> B 3<$（S=S1）<$B1<$B 2<$B3<$（S=S 2）B1<$<$BBOURAHLA和 BENMOHAMED12--⇒--作用tcγ（B3）。 换句话说，下面的含义应该是有效的（xp=xp yp）（xp > yp）。但是，决策程序无效这一点，因为它会导致模型中的错误，我们可以使用它的否定为了避免它，对于新的细化抽象模型，转换将像下面这样编写。（S=S 1<$B 3<$next（B3）<$next（S）=S 1）当我们对这个修改后的抽象模块进行模型检查时，我们得到了另一个错误跟踪（图4A），新错误跟踪中最后一个转换te的公式为：te（S=S1<$$>B 1<$$>B 2<$B 3<$$>next（B1）<$next（B2）<$<$next（B3）<$next（S）=S 1）当前抽象模型ta中的等效转换是ta（S=S 1B 3<$next（B3）next（S）=S 1）这是已经被修改过的抽象过渡。现在我们应用相同的规则如上所述，抽象变量B2将被采用。谓词next（B2）没有出现在当前转换中，因此我们必须验证（xp=xp yp）（yp > xp）也是无效的，可以消除从抽象的系统。第二个精化抽象模型的转换现在应该这样写（S = S 1 <$B 3 <$$>next（B 2）<$<$next（B 3）<$next（S）=S 1）。仍然有一个错误（图4B），它的轨迹给出了最后一次转换的公式te（S=S 1B 2<$B 3next（B2）<$next（B3）next（S）=S 1）这个公式以同样的方式修改，过渡ta（S=S 1<$B 2<$next（S）=S 1）为（S=S 1<$B 2<$<$next（B2）<$next（S）=S 1）现在错误跟踪（图4C）给出了公式te（S=S 0<$B 1<$$>B 2<$B 3<$下一个（B1）<$下一个（B2）<$下一个（B3）<$S=S 0）当前抽象系统中的等价转换是t a（S = S 0 <$B 1 <$S = S 0）.这个转换没有动作，所以我们可以取抽象变量B1、B2或B3中的一个。例如，我们取B1，精化抽象模型的新转换是（蕴涵真γ（B1）是无效的）（S = S 0 <$B 1 <$$>next（B 1）<$S = S 0）。因此，最后一个细化的抽象模型验证了具体化。BOURAHLA和 BENMOHAMED13∧⇒∧¬联系我们∧5.1细化算法在对示例执行了细化过程之后，我们给出了详细的算法。在对抽象模型进行模型检查后，每次得到错误跟踪路径时都会调用该算法。该算法不会引入新的谓词。它在不添加状态的情况下细化转换，因此这种细化方法是针对活性和可达性属性的。算法3改进设P为抽象错误跟踪的路径，当P不为空时，设te为抽象错误迹中最后一个变迁的公式，ta为抽象模型中相应的变迁也就是验证等式ta te=ta设A是具体谓词的抽象变量集合，使用在ta的等价具体转移tc的动作中出现的具体变量当A不为空时，从A如果（next（v） te=te）和（next（v）ta=ta）并且无效（actiontc γ（v）），则通过将ta修改为ta next（v）来细化抽象模型和返回elseif（<$next（v）te=te）和（<$next（v）ta有效（作用tc<$γ（v）），则A）不通过将ta修改为ta next（v）来细化抽象模型和返回结束if结束whileP：= P -最后一个抽象状态结束，没有可能的细化，那么在映射抽象错误跟踪之后输出具体的反例。因此，该算法的主要思想是在错误跟踪的最后一个抽象变迁中搜索不确定的抽象变量。然后它将这些变量一个接一个地取反它们的下一个值，这给出了一个细化的抽象模型（这是一个欠近似）。 如果这些变量不存在它将倒退，直到第一次过渡。最后，如果没有确定性变量，则使用函数γ产生具体的反例。6概述和实验图5显示了实现我们基于抽象-模型检查-精化的方法的工具的概述，该方法专用于无限状态系统的验证。BOURAHLA和 BENMOHAMED14解析器内部表示VHDL描述抽象符号模型检验细化映射错误跟踪具体错误跟踪满意的财产抽象系统图五、工具概述我们已经在Windows操作系统下实现了这个工具，并且我们使用了系统SVC（Stanford Validity Validity）[1] [16]的决策过程来证明定理。在执行抽象过程之后，我们调用系统SMV对生成的抽象模型进行模型检查。如果存在一个反例，我们称之为上述的精化过程，以在反例是虚假的情况下产生一个精化的新抽象模型。除了GCD的例子，我们还使用这个系统来验证Bakery协议中的互斥属性（这是一个安全属性，但不需要进行细化），并通过它测试了系统SMV中的VHDL及其等效物的进程间通信。Bakery协议由多个并行组件组成，每个组件用一个VHDL过程表示.我们还验证了ATM（异步传输模式）交换机[5]。这是一个相对较大的设计，它使用了许多组件。下表显示了我们对三种设计的实验。下表显示了使用的抽象变量的数量。它显示了为每个抽象生成和证明的含义的数量。还有改进的数量，以及验证的全局时间。情况#抽象变量调用决策程序的次数#优化时间（秒）GCD31842面包店33301.5ATM17254835表2实验结果BOURAHLA和 BENMOHAMED157结论我们提出了一种新的抽象细化方法，用于符号模型检查描述状态机的VHDL模型，这些状态机可以是无限转换系统。该方法由一个完全自动化的工具实现，包括一个谓词抽象的自动构造算法，通过该算法，我们将VHDL模型转换为等价的抽象SMV模型，以及一个有效的自动精化算法。当抽象系统的模型检查失败时的粗略抽象。这种改进算法逐渐消除了错误轨迹中的虚假路径。初始抽象系统的构造和精化过程使用了许多对决策过程的调用。精化算法中非确定性抽象变量的选择对精化算法的性能有很大影响，选择非确定性抽象变量的合理性将使精化算法的性能得到保证。引用[1] C. Barret，D. Dill和J.Levitt。对具有平等性的理论组合进行有效性检查。在Mandayam Srivas和Albert Camilleri，编辑，计算机辅助设计的形式方法（FMCAD '96），计算机科学讲义第1196卷，第187-201页，加利福尼亚州帕洛阿尔托，1996年11月。史普林格出版社[2] S. Bensalem，A.布阿贾尼角Loiseaux和J.Sifakis。财产保全模拟。在CAV[3] S. Bensalem，Y. Lakhnech和S.嗷计算抽象的无限状态系统组成和自动化。在Hu和Vardi [HV 98]，第319-331页，1998中。[4] S. Bensalem，Y. Lakhnech和H. 赛迪 自动生成不变量的强大技术。In R.Alberr和T.A. Henzinger，编辑，第8届计算机辅助验证国际会议，计算机科学讲义第1102卷，第323-335页。Springer-Verlag，1996.[5] T. Chaney，J.A. Fingerhut，M. Flucke和J.Turner。 千兆位ATM交换系统的设计。技术报告WUCS-96-07。华盛顿大学计算机科学系，圣路易斯，密苏里州，1996年。[6] E.M. Clarke，O. Grumberg，S. Jha，Y. Lu和H.维斯反例引导的抽象细化。Emerson和A. P. Sistla ， 编辑， 计算 机辅助 验证， 计算 机科学讲 义。Springer-Verlag，2000.[7] E.M. Clarke，O. Grumberg和D.E.久了模型检查和抽象。 ACM Transactionson Programming Languages and Systems，16（5）1512-1542，1994.[8] M.A.科隆和T. E.乌里韦使用决策过程生成反应系统的有限状态抽象在Hu和Vardi，第293-304页，1998中。BOURAHLA和 BENMOHAMED16[9] P. Cousot和R.库索抽象解释（Abstract interpretation）：一种统一的格模型，用于通过构造或近似定点来静态分析程序。在第四届ACM Symp.的Prog。浪第238-252页。北京：人民出版社，1977年。[10] D.水坝。模型检验的抽象解释和划分细化。博士论文，埃因霍温技术大学，1996年。[11] D.达姆斯河Gerth，G.多门河Herrmann，P. Kelb，and H. 帕格曼使用自适应状态和数据抽象的模型检查。在D.L. Dill，编辑，CAVSpringer-Verlag，Berlin，1994.LNCS 818.[12] S.达斯Dill和S.公园有谓词抽象的经验。在Halbwachs和Peled [HP 99]，第160-171页，1999中。[13] J. Dingel和Th. 菲尔科恩使用数据抽象的无限状态系统的模型检查在p.Wolper，editor，Computer Aided Verification，Volume 939 of LNCS，pages 54-69.Springer-Verlag，1995.[14] S. Graf和H.赛迪用PVS构造抽象状态图。在计算机辅助验证，卷1254计算机科学讲义，1997年。[15] R. P. Kurshan协调过程的计算机辅助验证。普林斯顿大学出版社，普林斯顿，新泽西州，1994年。[16] J.R.莱维特数字系统的形式验证技术。博士论文，斯坦福大学，1998年12月。[17] C.卢瓦索Graf，J.Sifakis，A. Bouajjani和S.本塞勒姆用于并发系统验证的属性保持抽象。系统设计中的形式化方法6（1），1995年。[18] D. E.久了模型检查、抽象和组合推理。博士论文，卡内基梅隆大学，1993年。[19] R.E. Harr和A.G.斯坦库列斯库VHDL在电路设计中的应用。Kluwer AcademicPublishers，1991.[20] K.L.麦克米兰符号模型检查。Kluwer Academic Publishers，Boston，1993.[21] H. Saidi和N.史恩卡抽象和模型检查，而你证明。在Halbwaks和Peled [HP99]，第443-454页，1999中。