基于SAT的实时系统抽象精化

理论计算机科学电子笔记182（2007）107-122www.elsevier.com/locate/entcs基于SAT的实时系统抽象精化Stephanie Kemper斯蒂芬妮·肯珀1，3Centrum voor Wiskunde en Informatica，阿姆斯特丹和r'eplatzer2，4美国宾夕法尼亚州匹兹堡卡内基梅隆大学摘要在本文中，我们提出了一个抽象的精化方法，使用SAT求解模型检查实时系统的安全属性。 提出了一种系统有界模型检测的忠实嵌入方法将时间自动机转化为具有线性算术的命题逻辑，并证明其正确性。有了这个逻辑表示，我们实现了一个线性大小的表示并行组成，并介绍了一个快速的abstrac-灰技术，工作一致的时钟，事件和状态。在必要时，通过分析虚假的反例，使用有前途的扩展反例引导的抽象细化与克雷格插值的语法信息来细化抽象。为了支持概括，我们的整体方法确定了基于逻辑的抽象细化所需的代数和逻辑原则关键词：抽象细化，模型检测，实时系统，SAT，Craig插值1引言汽车工业、铁路技术和航空电子的嵌入式系统中的故障通常会造成灾难性的后果。这些安全关键系统的一个主要特征是安全关键地取决于及时发生的反应。例如，列车控制器需要应用制动器作为对比当前轨道情况允许的速度更快的驾驶的响应。然而，这个响应必须在到达打开的门之前及时执行，否则它将是无用的。1本研究的一部分由荷兰BSIK/BRICKS项目资助2这项工作得到了德国研究委员会（DFG）的部分支持，作为跨区域合作研究中心“复杂系统的自动验证和分析”（SFB/TR 14 AVACS，见www.example.com）的一部分www.avacs.org，并得到了德国学术交流服务（DAAD）的奖学金。3电子邮件：s. cwi.nl4电子邮件：platzer@informatik.uni-oldenburg.de1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.09.034108S. Kemper，A.Platzer/Electronic Notes in Theoretical Computer Science 182（2007）107这些实时系统的无限状态空间引入的计算复杂性导致了可扩展性的严重限制，即使在非常完善的模型检查器中，如Uppaal（http://www.uppaal.com）。除了在有限状态模型检验中已经存在的全知状态爆炸问题[4]之外，当前用于实时系统的模型检验技术仍然局限于并发定量时间观测（由时钟测量）的数量。状态爆炸问题的一个特别引人注目的原因是时间自动机（TA）的并行合成通过形成叉积而获得的指数为了避免这种情况，我们定义了一个线性大小的并行组合的逻辑表示TA。通常，在满足性检查（SAT求解）期间，只有完整并行组合的减少部分必须从我们的表示中扩展非常复杂和优化的技术（例如，[10]）引导高端SAT求解器仅探索与特定安全属性相关的状态空间部分周围的非常窄的片段。 我们在此基础上 通过选择线性算术/命题编码（而不是从头开始为TA的受限域实现新算法）：这是一种已经成功证明其在有限状态系统中的巨大潜力的哲学[3]。在此基础上，我们利用时间自动机诱导的过渡系统的特殊性，使用抽象细化来处理无限状态的挑战时间自动机作为实时系统的流行模型，TA [1]是具有实值变量（时钟）的有限自动机的扩展，可以测量时间的流逝。它们的行为由一系列随时间发生的事件组成。 TA允许两种类型的事件：可见的（外部）和不可见的（内部）动作。 前者用于与其他自动机同步，而后者用于单个自动机的内部步骤，独立于其他自动机。 转变可以重置时钟并且被认为是瞬时的，即， 时间只能在自动机保持在其状态之一时流逝。触发转换和停留时间是由时钟约束限制的状态-分别称为警卫和不变量-当前时钟值必须满足。AVACS项目AVACS（复杂系统的自动验证和分析）项目致力于对复杂安全关键计算机化系统（如飞机、火车、汽车或其他人工制品）的模型进行严格的数学分析，这些系统的潜在故障可能危及人类生命。在这方面，我们实施了JAVA中的原型模型检查器，称为SAAT RE（基于SAT的Abs tractionRefinement）。作为SAT求解器后端，SAAT RE使用FOCI5，因为它能够导出插值，这在第5节的精化步骤中起着重要作用。[5]肯尼斯·麦克米伦（Kenneth McMillan）（根据[9]）。S. Kemper，A.Platzer/Electronic Notes in Theoretical Computer Science 182（2007）107109s可达s在k步中不可达Fig. 1. 基于SAT的抽象细化循环抽象细化循环的结构抽象细化[4，6]是一个有前途的研究方向，以克服 状态爆炸问题和无限状态模型检查的挑战，同时保持验证结果的正确性。抽象技术通过删除被认为与验证特定规范无关的约束来过度近似系统行为。如果抽象系统是安全的（没有错误状态是可达的），那么通过保守的过度近似，原始系统也是安全的。图1描述了抽象精化循环中数据流的概念概述（灰色框表示外部工具）。我们用线性算术表示命题逻辑中TA的转移特征，并自动产生一个更简单的抽象版本，在展开得到的转移公式（k次）后，满足性检查解决抽象系统中的有界可达性问题.根据结果，实时系统要么已被证明在界限k内是安全的（s不可达），要么需要再次使用SAT求解（FOCI）相对于抽象反例（具体化）进行分析。如果抽象反例在非抽象系统中有对应的反例，则实时系统是不安全的。否则，反例是虚假的，是不恰当的初始抽象选择的结果。分析反例（使用FOCI导出的Craig插值）有助于细化抽象并重新开始，直到系统被证明是安全或不安全的。相关工作Audemard等人。 [2]将TA的有界模型检查简化为数学公式的满足性问题。 他们详细阐述了TA的LTL特异性编码。但是，如果没有抽象技术，这种方法的可扩展性仍然是有限的。Jhala和McMillan [7]提出了一种用于谓词抽象的抽象细化方法。使用插值法，他们会考虑物业的特定特征而产生修正。然而，一个局限性是，他们的方法依赖于谓词抽象的谓词的适当选择。我们的方法可以被认为是一个快速的（因此，可扩展的）近似谓词抽象，谓词发现是显而易见的，利用TA的性质Clarke等人提出的抽象细化框架 [4]适用于源于有限状态程序的Kripke结构。相比之下，我们的方法处理了由实时时钟概念引入的无限状态模型检查的挑战。此外，我们直接使用一个公式表示为SAT为基础的有界模型检查。SAT求解器展开[k]具体化摘要病灶雷芬TA代表110S. Kemper，A.Platzer/Electronic Notes in Theoretical Computer Science 182（2007）107→/∈∨¬TAAA→׬ ∧ ∨- ∈ ∈{≥ ≤}本文结构在第二节介绍了实时系统和有界模型检验之后，第三节给出了TA在命题逻辑中的一个忠实表示，并给出了一个可靠性结果。在第四节中，我们引入了一个统一的抽象，并将第三节中关于可靠性的代数观点扩展到关于抽象的对应结果。第5节通过研究如何利用虚假反例来细化抽象来结束抽象细化循环，然后在第6节中总结和未来的工作。2个房间在本节中，我们将介绍TA [1]和有界模型检查[3]的标准概念，并给出我们的运行示例。时间自动机定义2.1[时间自动机]设是所有时间自动机的集合=（A，S，s0，X，I，E），• A是一组有限的（可见）事件，具有典型元素a，aJ;• S是有限状态集，初始状态s0∈S，典型元素s，SJ;• X是一组有限的（实值）时钟，具有典型元素x，y;• I：S→Φ（X）是将不变量分配给每个状态的映射;并且• ES（A）τ） Φ（X） （十）S是一组转换;其中（s，a，j，Y，sJ）表示在事件a发生时从s到sJ的动作转换，由保护时钟限制并重置集合Y中的所有时钟。时钟约束（即， 守卫和不变量）<$∈Φ（X）是具有时钟比较的命题逻辑公式，xyc和xc对于cQ，>，、、、，=，和常用的连接词，，. 时钟赋值ν是为每个时钟分配实值的映射，其表示自相应时钟上次重置以来所经过的时间。为了确保不变量在后续步骤中保持不变，假设它们是凸的（即，不包含，[1]），这是用于有效表示的重要属性（第3.2节）。特殊的不可见事件τA表示一个不与另一个自动机通信而发生的内部动作。TAA的迹语义迹A被定义为关联转移系统SA[1]的所有迹的集合：SA的配置（s，ν）由状态s∈S和满足不变量I（s）的时钟赋值ν组成S A的跃迁反映了可能随时间演化的方式：延迟跃迁（s，v）δ（s，v + δ）使所有时钟值增加相同的时间量δ，动作跃迁（s，v）a（sJ，vJ）在事件a上将Y中的时钟重置为零，并在沿（s，a，v，Y，sJ）∈E之后保持其他时钟不变，在该沿上，保护值对v为真。时间必须单调增加而不收敛（非芝诺迹线）。迹A，k被定义为A的迹的前缀的集合，（最多）长度为k。S. Kemper，A.Platzer/Electronic Notes in Theoretical Computer Science 182（2007）107111∈A¬执行联合广播通信的多个自动机的组合（注意[1]使用成对同步）形成了一个并行实时系统;其语义被定义为相应的乘积自动机的语义（我们在3.4节中提出了一种避免指数叉积的技术）。定义2.2[TA的乘积]设A=（A，S，s0，X，I，E），A=（A，S，s0，X，I，E）beTAwithXX =0。由于A和A的关系，TAAA，定义为AA=（AA， S×S，（s0，s0）， XX，I，E）• I（s，s）=I（s）I（s）and• 转换（s，a，n，Y，sJ）∈E和（sn，an，n，Yn，snJ）∈E均上升到：- （（s，s∈），a，n，Y，（sJ，s∈））∈E<$i <$a/∈A<$或a=τ（A的离散跃迁），- （（s，s），a，，Y，（s，sJ））∈Eia/∈A或a=τ（A的离散跃迁），- （（s，s），a， ，YY ，（sJ，sJ））∈Eia=a（synchronisation）.时间自动机有界模型检验（BMC）已被证明是验证安全属性的最有前途的方法之一[3]。其原理是检查过渡系统的前缀片段，并连续增加探索范围，直到它达到系统的直径（可计算的指标）-或发现了一个不安全的踪迹定义2.3[有界安全性]设A =（A，S，s0，X，I，E）是TA，设s∈S是错误状态。A在界k内相对于s是安全的，记为A| = k<$EFs，如果没有有限迹t k迹A，k，从s0开始，到s结束。否则，对于s来说是不安全的。在这些EF的可达性属性的基础上，其他有界LTL规范可以使用[2]中的编码来验证运行实例图2示出了众所周知的列车闸机控制器示例的稍微修改的版本（参见，例如，[1]）：列车有一个额外的状态（<列车只有在接收到“go”信号后才能通过闸门该系统的错误状态为停机，即，火车穿过（部分）打开的门3时间自动机接下来，设A=（A，S，s0，X，I，E）是TA。在本节中，我们构造了一个在命题逻辑中用线性算术表示A的转换关系的公式，A（A），它是根据从步骤t-1到步骤t的转换特征定义的。将得到的转换公式展开k次，得到一个变体（A）k，112S. Kemper，A.Platzer/Electronic Notes in Theoretical Computer Science 182（2007）107接近提高v<1离开出口v：=0v：=0慢火车低v≤1附近v≥2停止附近v<2去去≥一∈∈{}−一一出来接近远上下收盘没有火车火车接近门关闭出口X<5用gox：=0去近1（zt−1=zt）<$（xt−1=xt））在nb(a) 过渡<$（int−1<$outt<$ext−1 <$$>（zt−1−xt−15）<$（zt−1=zt）<$（xt−1=xt））(b) 过渡表示见图4。 表示：运行示例3.3有界模型检验为了在逻辑上表示BMC的可达性问题，展开了公式表示式A对于所有步骤1到边界k实例化。由此得到的公式（）k被称为的k-展开，并在（9）中定义（j/t表示-cf的局部化。第3.1节-t替换为j）。直觉上，令人满意的解释（或模型）对应于长度为k的A的迹，即，A的前k步的一种可能行为（3.6节）。defBMC相当于将<$A与ρ=s<$s<$.. A，然后A|=<$EFs保持K我认为这种结合是不满意的。k01k k3.4并行系统在 本 节 中 ， 我 们 介 绍 了 TA 系 统 的 线 性 大 小 逻 辑 表 示 ， 而 不 形 成 指 数 叉 积（Def.2.2）。在并行实时系统中，自动机对可见事件（= τ）执行联合广播同步：如果事件a发生，则每个具有A i（“知道a“）的自动机i必须执行标记为a的转换，或者如果a，则执行零延迟步骤（“无”）。 相反，如果事件τ发生，自动机可以决定执行标记为τ的转换或执行零延迟步骤。 延迟d>0的延迟步骤必须由所有自动机同步执行。乘积表示只是各个表示的结合，其中（6）被理解为是所有事件的统一，因为在任何时候，在时间上，只有一个事件可能发生。3.5讨论命题公式作为中间表示有几个优点：最重要的是，我们的方法可以使用高性能的SAT求解技术进行验证。其次，它很容易推广到其他基于过渡的系统，如混合自动机[5]。一旦定义了到公式的转换（此外，我们的代表是专门为SAT解决技术定制的。除了尽可能提供合取范式（CNF）之外，还可以看到（5）和（6）是二元子句，它们非常有效（2-SAT问题是多项式的，因为二元子句不会增加搜索空间的宽度）。公式（7）也对应于一组二元子句，而（4）产生单位子句。请注意，将我们的表示调整为对数表示是立即的。S. Kemper，A.Platzer/Electronic Notes in Theoretical Computer Science 182（2007）107115一AA∈ϕA（A）kTR\ςModTraceA，kMod（n（A）k）ζ图五. 表示的正确性状态和事件的编码。在命题逻辑中，利用加法进位编码，互斥可以用线性子句数表示真实的状态变量加起来等于1 然而，尽管有这种理论上的优势，但在实践中更喜欢哪种变体并不明显，因为与线性表示-（5）限制于二元子句。而由于转移选择的选言性质，（3）不在CNF中，当引入新符号时，它可以直接转换为短CNF。对于并行系统，我们的逻辑表示避免了指数积构造，并且在数量上是线性的自动机。3.6正确性为了使表示法（）是忠实的（即，表现出与）相同的行为，每个模型都必须对应于长度为k的迹，反之亦然。这在下面的定理中得到了形式化的描述（参见[8]的形式证明）：定理3.3（表示的正确性）TA表示是正确的，即，图中的图表 5通勤6.在这里，交换性质表示，模型A（A）k具有与原始TAA的迹的双射对应，由对应映射A和A表示：模型A（t）的迹A（t）属于某个迹t迹A，k再次是t（即，并且属于某个模型m∈Mod（<$A）k）的迹<$A（t）的模型<$A（m）也是m（即，（4抽象在本节中，我们将介绍一种简单、快速但功能强大的统一抽象技术，专门针对逻辑公式：合并省略抽象（MO）。通过去除被认为与特定安全属性无关的约束，MO产生过近似。4.1合并省略抽象MO的基本思想是通过减少系统的数目来降低系统的复杂度。在保留尽可能多的关于跃迁特征的信息的同时，尽可能多地保留符号的数量（尽管抽象公式比符号的数量（A）弱）。是图是可交换的[12]，在图中的每两个节点之间，沿着每一条路径都会产生相同的结果。例如，Mod（λ（A））=λ（tr（A））或λ（Mod（λ（A）=tr（A）。116S. Kemper，A.Platzer/Electronic Notes in Theoretical Computer Science 182（2007）107∪一一作为一一一¬¬作为α（L）L⎨如果（L）（AS）=γ（L（⎩真否则ifcont（L）=0， Lposiveα（F<$G）=α（F）<$α（G）α（F<$G）=α（F）<$α（G）这里，F和G是NNF中的公式，L是一个文字，而（L）是在L中出现的原子公式和变量的集合。定义为否定范式（NNF）的公式，这已经适用于NNF（）（可以很容易地将guards转换为NNF）。在续集中，让=（A，S，s0，X，I，E）一个TA，让A=AS命题字母的集合（状态和事件，没有索引）;实变量的集合（时钟参考）是X。为了说明抽象对不同语法范畴的影响，我们用状态事件映射γ（称为合并映射）和时钟抽象集（称为省略集）来定义它定义4.1[合并省略的抽象]设F是NNF中的公式，命题字母为X，实变量为X。设AS <$Φ（X）<$X是一个不含复合公式的集合，γ：<$→ <$J是到某个命题字母集合<$j的映射，其中<$J=<$. 通过应用变换α来定义相对于AS和γ的F的合并省略的抽象作用;如图所示。六、见图6。 合并省略将α提升到局部化的存在是简单的：γ和被理解为忽略了NNF中的索引，使得索引直接保持不变地传递到NNF（）k（使用相同的α定义来定义不同步骤的不同抽象是可能的，但我们认为它不太有用）。MO一致地捕捉到命题字母和关于这些字母的实变量或原子谓词的抽象（因此能够抽象3.1节中定义的所有符号）。映射γ是不打算抽象的符号的恒等式。然而，具有相同图像的状态（或事件）被合并。通过这种方式，α执行了存在抽象的快速变体[4]，但利用了时钟和TA的结构关系。此外，α关于{，}是同态的，这证明了α（（A）k）和α（（A））k相等（除了计算抽象的速度，其中α（（A））k更优越）。注意，与负时钟约束不同，α总是将负比例字母映射为true。一般来说，这是必要的，因为s不允许在合并γ（r）= γ（s）= u的情况下得出u。对于我们的设置，无论如何，在应用α之后，重新生成包含负命题变量（特别是（5）和（6））的那些部分是更有效的。S. Kemper，A.Platzer/Electronic Notes in Theoretical Computer Science 182（2007）107117AS∈AAAA→i−1→i−1我 我i−1→i−1我 我我我4.2运行实例考虑图4（b）中的公式。如果x，MO用真替换所有包含x的（原子）子公式，公式最终简化为（outt−1<$fat<$apt−1 <$$>（zt−1=zt））<$（nbt−1<$int<$got−1<$（zt−1=zt））<$（fat−1<$nbt<$nrt−1 <$$>（zt−1=zt））<$（int−1<$outt<$ext−1<$（zt−1=zt））注意，即使时钟x被抽象，它也对可以保留的迹线施加了限制：在后续事件接近和退出之间，时钟值最多可以增加5。这些信息可以添加到控制器自动机中，以约束其行为，从而提高效率（见5.5节）。4.3正确性为了使α产生正确的过近似，具体系统的每个有限迹（由一个模型表示，见定理3.3）必须在抽象情况下是可再现的，这是由下面的引理建立的（见[8]的形式证明）。引理4.2（弱化抽象）抽象MO产生一个保守的近似，这意味着在蕴涵F→α（F）有效（在所有模型中为真）的意义上，α（F）弱于F。为了将我们的逻辑抽象细化方法与TA上的抽象联系起来，并强调结构关系，我们证明了比引理4.2所表达的结果更强的正确性。为此，我们使用具体和抽象系统之间的同态对应[4]。定义4.3[迹的同态]令和 beTA，withX X，Letγ：SASAasurjection. A函数h：T raceTRACE对于ea ch迹t∈TraceA，存在一个迹Aeh（t）=t∈Trac e h，使得（a）对i≥0，t和t中的第i个构形（si，νi）和（si，νi）分别为A时，满足：γ（si）=s<$i，且νi和ν<$在公共变量上一致，且（b）对于i≥1，阿一阿二第i步（s， ν ）（s， ν）和（ s，ν）（s，ν）满足：γ（a）=a（accord-（图为无限的痕迹）。从代数的角度来看，更强的结果甚至可以直接从引理4.2中得到，因为α在局部起作用，因此保留了（9）的公式结构。定理4.4（抽象的正确性）MO，如定义4.1中所定义的，产生一个正确的过逼近迹集。为了证明具体迹和抽象迹之间的同态的存在性（详见[8]），图的上半部分7被示出为交换图，这样，根据组成，hT的存在是一个直接的结果。这一命题的思想如下：当α保持f（9）的形式时，存在一些自动机A，118S. Kemper，A.Platzer/Electronic Notes in Theoretical Computer Science 182（2007）107II我III一一AAA.A.ζϕA（A）kϕ（Atr\ModςModTraceA，kMod（（A）k）Mod（（A）k）T raceA，kςhT见图7。 抽象的强正确性相同的表示<$（）k=α（<$（）k）（直到逻辑等价）。因此，在本发明中，图7中标记为（i）和（iii）的子图根据定理3.3可交换。标记为（ii）的子图根据引理4.2进行交换，因为每个<$A（k）的模型都是α（<$A（k））的模型因此，整个图是上下班的。4.4讨论由于α的一致性，我们通常不必区分状态抽象、事件抽象和时钟抽象的单独处理。在逻辑层面上，这些只是碰巧代表不同自动机概念的任意符号。特别地，代数观点甚至允许从强正确性结果得出结论，在TA上有一个相应的有效抽象技术（与逻辑公式相反），它产生了证明（上面的证明是简单的，但非建设性的）。然而，证明这种技术是正确的（甚至陈述它）将比我们嵌入逻辑所能表达的要复杂得多，也不那么统一。7说明了逻辑抽象和自动机上的抽象的相互作用因此，我们在普适性和效率之间取得了很好的平衡：每个满足引理4.2的抽象α在我们的框架中已经被证明是正确的，这使得它成为一个强大的技术。 由于纯粹的语法定义，它是非常有效的，虽然。5抽象细化在本节中，我们将介绍我们的通用抽象细化方法，遵循通用抽象细化范式[4]：（1）生成初始抽象，（2）对抽象系统进行模型检查，以及，如果需要，（3）细化抽象（参见。图1）。我们讨论了如何检测虚假反例，以及从虚假反例中可以得到什么样的信息来找到一个适当的改进。5.1生成初始抽象如果没有关于系统的额外知识，则初始抽象简单地将包含在Φ（X）X中的所有符号从Φ（）中移除，并合并S中的所有符号。到一个单一的（我们参考[4]的改进技术），从而崩溃到一个αζS. Kemper，A.Platzer/Electronic Notes in Theoretical Computer Science 182（2007）107119一A.作为→甲磺酸∈一个一个一def一个平凡的状态（相应地对于A）。然而，下一次迭代的细化将很快发现更多相关的参数。5.2抽象系统在抽象之后，检查α（（））kρk 如果它是不可满足的，则系统在界k内是安全的（3.3节和4.3节）。相反，如果SAT求解器返回一个令人满意的模型（对应于定理3.3中的反例迹），则设π为根据该模型的变量赋值的合取。这个抽象的反例需要具体化，即，翻译回具体系统的术语，并检查可行性，这相当于满足性检查（）kρkπ。对于状态s，sJS，其中γ（s）= γ（SJ）= u，我们进一步将具体化约束USSJ加到π上，它表示只要π在u中（相应地对于事件或多个状态），要么在状态s中，要么在sj中。因此，单个抽象反例迹对应于（可能是几个）的迹，其特征在于形成γ对状态和事件的原像的析取。观察到时钟约束在该过程期间保持不变，因为时钟的值从抽象反例中是未知的（如果丢弃，即，）或不变。由于π是高度限制性的（它只挑出一条抽象的路径），抽象的反例以非常狭窄的焦点引导对具体系统的搜索，并且非常有效（5.5节）。如果kρk π是满意的，这就产生了一个具体的反例。否则，π是伪的，抽象必须被细化（见5.3节）。5.3提炼抽象我们使用SAT求解器（FOCI）提供的Craig插值（例如[9]）来识别抽象不良的参数。一对不一致公式（A，B）的克雷格插值是一个公式C，它被A（C的前缀）所隐含，与B（C的后缀）不一致，并且只引用A和B的公共符号。因此，C是A的联合过近似和<$B的联合欠近似。1999年，张继伟（ ）k，π和ρk（即， 沿展开深度k），我们推导出一个插值为每个分区到prefix和sufix。由此，我们得到了一个强插值序列（参见[8]）对于细节），使得存在最后一个插值G 错误。 根据定义，前缀一个虚假的内插是不满意的。 因此，π的相应前缀表示在A中不可具体化的迹线。如果有一个整数p=true，则可以求出由G_n和G_n之间的模所表示的子迹，因为真正的插值表示没有任何信息可以从跟踪前缀传递到这个索引。 此外，当P表示所有可抽象的符号的集合时，我们知道IA=n（G）nP中至少有一个符号没有被充分抽象。因此，有两种细化选择： （a）从IA中提炼一个符号，或者（b）通过添加以下项来排除由G120S. Kemper，A.Platzer/Electronic Notes in Theoretical Computer Science 182（2007）107低τ提高≤∧作为/AS≥- ≥上平仓无列车列车接近门关闭门：开口下来控制器：接近，v：=0降低，v≤1慢火车附近v≥2见图8。 优化：运行示例一个对应的连词（CEGAR in [4]）。虽然（a）是合理的（cf. 第5.1节），过早地对（a）进行修正，会过早地坍塌到混凝土系统，从而减慢整体验证速度 另一方面，策略（b）非常简单，但是只要基本参数没有被充分地提取，就会导致大量的虚假反例。我们已经确定了以下全自动启发式算法作为这些替代方案之间的折衷：在细化参数（a）之后，规则了固定数量的迹线（展开深度k的分数被证明是最有希望的）在根据（a）细化下一个符号之前，通过（b）进行输出。进一步的优化包括跟踪到目前为止发现的所有反例，并在IA中首先细化最频繁出现的符号。同样，作为一种清理策略，（b）添加的反例可以在其签名被（a）的后续细化覆盖后删除。5.4运行实例为了简单起见，设合并γ的映射是恒等式，并设omis的集合是Ssions包含时钟y（singleton）。图8中所示的门和控制器自动机的部分显示了这种情况，其中可以达到打开慢速列车的状态（因此也是错误状态）。 然而，具体化该轨迹是不可能的，因为在图2的相应部分内，始终保持y v（这避免了在从关闭到关闭之前在接近上同步），并且SAT求解器返回插值序列。我们知道最后一个插值G=false将包含时钟y7（参见第5.3节：是单例的，因此只有y可以导致伪反例），因此y必须被精化。注意：在验证较大的系统时，这些系统不会崩溃为具体系统，但我们的方法正确地识别了抽象参数。5.5初步实验结果一些初步的实验结果描述在表中。1.一、从第5.1节中描述的初始抽象开始，Tab. 1表明我们的整体抽象细化技术非常快，因为主要的运行时间都花在（外部）SAT求解器调用上（83%）。我们的抽象细化框架的效率增益通过观察指出，最后一次迭代，即，当所有相关参数（除了时钟x）都已被我们的精化确定时，需要不成比例的时间。因此，第一次运行是为了7例如，插值可以包含约束（ztYT2），表示在步骤T中时钟Y必须大于2，以便该轨迹是可具体化的。S. Kemper，A.Platzer/Electronic Notes in Theoretical Computer Science 182（2007）107121例如在战略8完整运行其中：SAT求解器调用此处：上次迭代第2节1/2k16：88914：594八点一百六十三分第4.2节1/2k十六点六百三十一分十四点三百三十四分七点八六六第2节1/ 3千十五点六五一13：081五点四百四十五分第4.2节1/ 3千16：957十四点四百三十九分六点四二三第2节1/4k十一点三百一十二分九点六百六十五分六点六百六十五分第4.2节1/4k十一点零三分九点四百五十一分六点二百七十九分表1TGC实例相比之下，速度很快。使用推断信息（4.2节）加强α至少会略微改善性能。选项卡.1还表明，效率取决于所选择的启发式。6结论和今后的工作在本文的背景下，我们提出了一种基于SAT的方法，用于TA并行系统的抽象精化模型检查我们定义了一种将TA系统的有界模型检验嵌入到具有线性算术的命题逻辑中的方法，并引入了一种基于统一逻辑的时钟、状态和事件抽象。这种逻辑表示直接受益于SAT求解器的最先进技术，并允许并行组合的线性大小表示。除了证明表示和抽象的正确性外，我们还仔细识别抽象细化方法背后的代数和逻辑原则。我们希望这些结构关系能够提供一个模块框架，将我们的工作推广到其他场景（如混合自动机），而无需从头开始除了这些概括之外，未来的工作还包括案例研究中我们实现的性能比较，以及选择对数编码状态的效果分析（尽管在这种情况下，状态抽象稍微多一些）。使用SAT求解器可以提高整体性能，该SAT求解器针对具有伪布尔约束或同构推理的有界模型检查而定制。此外，我们打算检查不同的设置，以平衡反例引导的抽象细化与基于克雷格插值的细化。作为一种普遍的哲学，我们建议扩展我们对当前模型检测研究中的代数关系的研究，以便（a）适当地确定结构原则，（b）建立一个稳定的框架，用于概括更高级的验证问题，例如：[5]。确认这 项 工 作 的 早 期 版 本 受 益 于 与 AVACS 成 员 的 讨 论 ，特 别 是 Ernst-Ru？digerOlderog，MartinFr？nzle，HenningDierks，An？8策略表示在细化下一个参数与展开深度k122S. Kemper，A.Platzer/Electronic Notes in Theoretical Computer Science 182（2007）107德列亚斯·波德尔斯基和安德烈·雷巴琴科。引用[1] 巴尔河， 时间自动机，in：N.Halbwachs和D.Peled，editors，CAV，LNCS1633（1999），pp.八比二十二[2] Audemard，G.，A. Cimatti，A. Kornilowicz和R. Bounded Model Checking for Timed Systems. ，in：D.Peled和M.Y. Vardi，editors，FORTE，LNCS2529（2002），pp.243-259[3] Clarke，E.，A. 比耶河Raimi和Y.Zhu，Bounded Model Checking Using Satisfiability Solving。系统设计中的形式化方法19（2001），pp.7比34[4] Clarke，E.，O. Grumberg，S. Jha，Y. Lu和H. Veith，Counterexample-guided abstraction refinementfor symbolic model checking。，J. ACM50（2003）.[5] Henzinger，T.，混合自动机理论。，in：LICS，1996，pp. 278-292.[6] Henzinger，T.，R.贾拉河Majumdar和K. McMillan的Abstractions from Proofs。，in：N. D.琼斯和X.Leroy，editors，POPL（2004），pp.232-244。[7] 贾拉河和K. McMillan，基于插值的