理论计算机科学电子笔记144（2006）19-33www.elsevier.com/locate/entcs用可满足性模理论对Lustre程序进行AndersF ranz'en1文凭Informatica eInformaciónUniversit`adiTrento意大利特伦托摘要利用整数运算验证Lustre程序的安全性问题已经受到了各种各样的攻击。NBAC使用抽象解释，Luke使用SAT求解器进行本文提出了一种使用可满足性模理论（SMT）作为Lustre程序的增量式判定过程的方法。我们表明，即使是一个非常天真的方法，使用SMT是有竞争力的，在某些情况下，其他方法的补充关键词：光泽，形式验证，时间归纳，满足模理论1介绍近年来，一种新的一阶逻辑的可判定片段的判定过程在通常被称为可SMT可以被看作是命题逻辑的满足性的扩展，在特定的理论中有约束，例如整数或实数上的线性算术这些逻辑的决策过程的一个常见方法是扩展一个普通的SAT求解器，使其具有处理理论中约束的能力这是CVCLITE[1]、DPLL（T）[12]、haRVey[7]和MATH SAT[3]等系统中使用的方法一些系统，如ARIO[19]使用伪布尔SAT求解器，但仍然使用相同的原理。1电子邮件地址：anders@dit.unitn.it1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.07.01720A. Franzén/Electronic Notes in Theoretical Computer Science 144（2006）19ax≤biii联系我们在这里，我们将展示如何用简单的方法构造一个增量SMT过程，以及如何将该过程用于Lustre[15]程序的归纳由此产生的程序将被证明是在许多情况下的性能与使用其他方法的工具，并在某些情况下优越。1.1可满足性模理论可满足性模理论（SMT）是检验无量化一阶公式关于特定理论的可满足性的问题。这里感兴趣的理论是线性算术表达式上的无量化关系，其中所有变量都被约束为整数。在不失一般性的情况下，我们可以将自己限制在这些类型的关系中：iai xi=b其中xis是自由变量，ai和b是（整数）常数。在本文中，这样的关系将被称为约束然后我们可以创建这样的公式：（x≤0y≤ 0）−y≤−1x= 0<$（P→x≥0）<$（<$P→x≤−1）其中x和y是整数变量，P是命题变量（0元谓词）。在迭代算法中确定公式的可满足性一个SAT枚举器，它解释为纯粹的proposi- tional公式，并枚举所有满足命题变量和约束的真值分配然后在整数线性算术理论中检查这些是否满足。举个小例子，x= 0<$（P→x≥0）<$（<$P→x≤−1）SAT枚举器可以从模型x= 0，P，x 0，x 1开始。 在整数线性算术平均理论中检查该模型的满足性，以检查系统x= 0时x≥0x≤−1A. Franzén/Electronic Notes in Theoretical Computer Science 144（2006）1921--关于我们有一个解决方案。 它没有，所以SAT枚举器创建了一个新的命题模型，比如{x = 0，P，x ≥ 0，<$x ≤ −1}。现在系统x= 0时x≥0x≥0必须检查，因为它是满足的，公式是满足的，我们可以通过将上述约束问题的解决方案与SAT枚举器的命题模型合并来创建一个模型。SAT枚举器通常被实现为SAT求解器，并且通过向SAT求解器所持有的命题公式添加描述不满意原因的“冲突子句”来请求新模型，从而禁止重复出现1.2Lustre编程语言Lustre是一种同步声明语言，其基本数据抽象是流。Lustre程序是一个节点，具有零个或多个输入流和一个或多个输出流。流是一个值序列，Lustre支持布尔、整数和实数流。节点也可以有内部流。作为一个简短的例子，考虑这个Lustre节点。NodeAddIf（X：int，B：bool）返回（Y：int）;让Y =如果 B则 X+1否则 X;电话该节点具有两个输入流X和B以及一个输出流Y。 给定输入流X= 1，2，3，4，5，.. . 而B=假，真，假，真，假，. 我们将得到输出流Y= 1，3，3，5，5，.. . .关于Lustre语言的更多信息可以在[15，14]中找到2的基本程序我们将使用的验证方法是时间归纳法[18，2]，这是简单的深度随时间的归纳法，有一个小的增加，使其对有限状态系统是完整的。归纳证明由两部分组成：基本情况，我们证明该属性在第k个状态中成立;步骤情况，我们证明如果它在k个连续状态中成立，它也在下一个状态中成立。对普通归纳法的必要修改是，我们需要在阶跃情形中要求状态是唯一的。22A. Franzén/Electronic Notes in Theoretical Computer Science 144（2006）19→在这里，我们将使用这个过程来验证安全属性的光泽程序与无界整数。这创造了一个无限状态系统，对于这个系统，归纳是不完全的。就Lustre而言，这并不像看起来那么坏事实上，有无界整数的Lustre是图灵完备的[11]。这意味着没有完整的方法来验证具有无界整数的Lustre程序。有几种可能的归纳方法，我们这里使用的归纳方案是ZigZag[10]。为了支持无界整数，将使用扩展了整数上的线性约束的命题逻辑的判定过程2.0.1光泽词语布尔流可以直接转换为转换函数的逻辑描述。例如，逻辑或运算符p=a或b可以转换为（<$ap）（<$bp）（abp）转换整数流需要多一点小心。要了解原因，让if-then-else表达式如下所示e=ifbthene1elsee2这些可以直接翻译成b→e=e1<$b→e=e2但这是不必要的，因为当SAT求解器给b赋值时，只有表达式e1和e2中的一个是相关的，这意味着只有一个等式应该被检查是否满足。这里使用的解决方案是使用保护约束g c，其中g是称为保护的命题变量，c是约束。这将使得忽略约束成为可能，因为当SAT求解器将guard赋值为false时，相应的约束与公式的可满足性无关一个if-then-else的公式可以（简化）为b→g1 <$g2<$b→< $g1<$g2g1→e=e1g2→e=e2A. Franzén/Electronic Notes in Theoretical Computer Science 144（2006）1923→一般来说，这并不意味着限制约束问题的大小，而是限制那些与if-the-else表达式中条件的真值分配相关的约束问题由于上面的e1和e2可以包含任意整数表达式，包括if-then-else表达式，因此我们希望能够忽略这些表达式中出现的所有约束。关于这一点的描述可以在[11]中找到转换从解析树开始，其中属性（布尔Lustre流）位于根。首先深度遍历解析树，依次翻译每个节点。永远不会创建带有保护约束g c的子句。相反，在解算器中维护防护与其相应约束之间的映射。对于由SAT求解器构造的每个命题模型，检查守卫的一个约束问题是从约束的警卫是真的模型。如果约束问题是满足的，则可以通过将命题模型与约束问题的模型相结合来构造模型否则，从约束问题中提取不满意的原因原因是导致不满意的约束的子集。在SAT公式中添加了一个子句，该子句包含对原因中约束的保护的否定，禁止SAT求解器再次生成相同的（希望是许多类似的）模型为了获得好的性能，从不满足的约束问题中提取一个好的理由是至关重要的。2.1分析不可满足约束问题在整数线性规划文献中，检测不满足约束问题的原因的问题是众所周知的。一个最佳的理由被称为IIS，或一个不可行的不可约系统，其中可行性是满意度的同义词。定义2.1不可行不可约系统（IIS）是不可行约束的最小集合。这意味着一个系统是一个IIS• 这是不可行的（不满意的）。• 不可能在不使其可行（满意）的情况下从集合中移除任何约束。任何不可行的系统至少包含一个IIS。让我们看几个例子。24A. Franzén/Electronic Notes in Theoretical Computer Science 144（2006）19----系统(1)x1>0(2)x2−2x1 = 1(3)x2≤1是IIS，因为它是不可行的，并且不可能在不使其可行的情况下删除任何约束。系统(1)x1>0(2)x2−2x1 = 1(3)x2≤1(4)x10<另一方面，它不是IIS。可以在不使系统可行的情况下去除2和3注意，如果删除4，则不能删除2或3。这意味着该系统有两个IIS，1， 2， 3和1， 4。也可以让IIS只有一个约束，如本例所示：2x = 1该系统没有任何整数解，因此它是不可行的，是一个IIS。对于线性规划问题[6，5]和非线性规划问题[13]，有几种方法可以发现IIS。大多数为线性规划设计的程序也适用于非线性规划[11]。这里我们将使用一个非常简单的算法。由于在IIS中，不可能在不使系统可行的情况下删除任何约束，因此我们可以尝试逐个删除问题中的约束如果一个约束可以被移除而不使系统可行，我们就知道剩下的约束至少包含一个IIS。如果不是，我们知道我们最后删除的约束是IIS中的成员，必须被替换。这算法被称为删除过滤。在约束问题中经常有几个IIS，然后删除约束的顺序决定了哪些IIS将被识别。这里选择的顺序是从Lustre转换时创建约束的顺序这样做的动机是，我们想要一个尽可能与属性密切相关的原因。翻译是在解析树中深度优先完成的，属性位于根，选择的顺序似乎与我们想要的非常接近一般来说，要在约束问题C中找到IIS，A. Franzén/Electronic Notes in Theoretical Computer Science 144（2006）1925≤±≤Xk=i/=akixi+b。算法需要解决一个约束问题的每个约束在C。这可能是非常昂贵的，还有其他更有效的算法。特别是，据报道弹性滤波算法[6，5]更有效。尽管如此，删除过滤在这种情况下可以很好地工作[11]。3一个简单的不完全约束求解器搜索过程中产生的大多数约束问题都是不可满足的。这并不奇怪，因为只要找到一个可满足的约束问题，就足以因此，能够有效地检测不满足的约束问题是很重要的。这些问题中的大多数都有非常简单的“约束”，一个便宜的程序将能够检测到这些问题，而不会产生整数线性规划的全面约束求解器的成本。本节描述了这样一个廉价的程序，它可以检测一种简单的不可满足的约束问题，并找到这些问题的近似原因。3.1预赛我们对所有变量都有一个全序。 一个全序是这样的，如果i j，那么要么vi<$vj要么vj<$vi。约束是在范式上的，如果最大公约数gcd（a1，...，a n，b）的因素和右手边是1。任何约束都可以通过将每个系数和右手边除以gcd（a1，...，a n，b）。等式是一个定义，如果最大变量的系数（在Chosen可变序中）是1或-1。定义可以改写为3.2该算法基本思想是如果我们有两个约束条件x b1x>b2这两个约束条件是不可行的b2. 一个使用这个事实的算法一次只取一个约束，通过应用所有已知的定义并消除一些变量来简化它。如果新的简化约束为一个定义，这个定义适用于所有已知的约束，消除一个变量。然后将新约束添加到已知约束集合中。如果任何一对已知的约束的形式x b，相互矛盾，一个不可行的检测。该算法可以26A. Franzén/Electronic Notes in Theoretical Computer Science 144（2006）19∈←∅- ≤−算法1检测不可行性要求：C是一组约束不对于所有的cc做使用T中的所有定义来简化c如果c是一个定义，简化T中的所有约束，定义为cend ifT←T {c}如果T有一对（x≤b1，xb2），其中b1b2，则返回不可行如果结束，则结束返回未知通过跟踪简化约束时使用的定义来找到不可行性的解释。当发现一对相互冲突的约束时，除了这对约束之外，还有直接或间接用来将这两个约束简化为最终形式的定义。当过程检测到不可行性时，可以继续从约束集中添加约束，可能会发现更多不可行的子系统。对于每个SAT模型，可以尝试这种不完整的过程。只有在无法找到冲突的情况下，才必须使用更昂贵的程序。4一种增量SMT工艺上面描述的过程是用增量接口实现的，因为它将用于归纳验证。增量SAT求解器MiniSAT [9]已扩展为SMT过程，给出了具有以下类似C++伪代码的接口的过程。Var addPropositionalVariable（）;向求解程序添加新的命题变量Var addGuardedConstraint（约束c）;将新约束添加到求解器并返回其保护（命题变量）。A. Franzén/Electronic Notes in Theoretical Computer Science 144（2006）1927voidaddClause（List Literal> clause）;<将子句作为文字列表添加到求解程序。boolsolve（List Literal> assumptions）;<解决问题。该方法确定在假设中的所有文字均为真的假设下，到目前为止添加的一组条款是否如果公式是令人满意的，它的模型可以检索。表示不满足约束问题的原因的约束子句被永久地添加到SAT求解器中。这样做部分是为了确保完整性，部分是为了简单。5实验评价一个名为Rantanplan的工具[4]基于这里提出的想法，已经与两个竞争对手进行了竞争：NBAC2，基于抽象解释[17]，以及Luke3版本0.4beta的修改版本。Luke是一个基于归纳法的程序，它使用了一种对SAT求解器的渴望编码。Luke的修改包括SAT解算器从Satnik交换到MiniSat[9]。Rantanplan 基 于 Luke ， 并 与 Luke 共 享 大 部 分 代 码 该 程 序 可 从http://www.dit.unitn.it/获得，包括用于评估的测试套件5.1实验装置测试是在一台配备Intel Xeon 3GHz处理器、1024 kB高速缓存和4 GBRAM、运行Linux的计算机上进行的。 NBAC使用以下标记运行：+eliminput --cudd“-maxRight 128”由于某些示例超出了默认限制，CUDD的内存限制已增加到128 MB。+eliminput是必要的，因为某些属性与当前时间点的输入信号有关Luke用命题字面量来表示整数位向量这些位向量的大小可以由用户更改，对于这些测试，Luke使用默认的16位整数运行。对于简单的问题，整数的大小不会对性能产生足够的影响，从而改变结果。2这里使用的是2004年11月3日发布的无界整数版本3在编写本报告时，可查阅http://www.cs.chalmers.se/Cs/Grundutb/Kurser/form/luke.html。28A. Franzén/Electronic Notes in Theoretical Computer Science 144（2006）19工具已验证独自验证NBAC9618卢克981兰坦普兰1061表1由不同工具验证的属性数量这些实验中的困难问题即使对于非常小的整数也是困难的，因此位向量大小的选择并不重要。5.2测试套件描述测试套件由许多Lustre程序以及程序上的测试是一个程序/属性对。由于许多程序都有几个属性，所以同一个程序会被用于几个测试。对于具有多个属性的程序，也有一个测试，其中属性是程序上所有属性的合取。测试套件完全由Lustre程序的学术示例组成例如，有几个是高速缓存一致性协议的模型[8]。这些测试的选择是为了让它们可以用任何工具进行验证，只要有足够的时间。那些无法用一种或多种工具验证的测试已经被删除。所有测试结果的概述见表1.一、值得注意的是，在测试套件中的127项测试中，有7项未通过任何工具验证。在这127个测试中，只有72个可以用于比较执行时间。有三个原因导致测试被排除在外：• NBAC无法处理无效属性。Luke和Rantanplan之间关于无效属性的一个小的比较可以在5.3.1节中找到。• 对于Luke和Rantanplan来说，某些Lustre程序的某些属性不能单独验证，而只能与该程序的所有其他属性一起另一方面，NBAC一次只能验证一个属性，因此很难比较性能。• 有些性质对无界整数有效，对有界整数无效，如路加福音中所建模的。其余72项测试的复杂程度各不相同。所有测试都相当小，如图1所示，它显示了测试的整数和布尔变量的数量。测试运行超时100秒。结果以累计完成率的形式列示。这是从测试套件中随机选择的测试作为时间函数终止另一种解释A. Franzén/Electronic Notes in Theoretical Computer Science 144（2006）19293025201510500 20406080 100 120布尔图1.一、示例中布尔和整数变量的数量图二、所有Lustre示例的结果数据是，它是终止测试的比率作为时间的函数。如图2所示，有一组测试NBAC和Luke都在挣扎。在这一组中，我们发现测试更复杂的算术。这些测试包括两个或多个整数变量之和的算术表达式，而其余的只包含其中一个操作数是常量的简单算术表达式删除NBAC或Luke中花费超过10秒的示例，数据如图3所示。整数30A. Franzén/Electronic Notes in Theoretical Computer Science 144（2006）190 2 4 6 8 10时间（秒）图3.第三章。简单Lustre示例的结果5.3解释差异NBAC和Luke遇到麻烦的例子都有一个共同点：它们在表达式中使用两个或多个变量的和。所有其他的例子都只是对变量加上或减去一个常数。NBAC也有几个属性的结合的麻烦，其中基于感应的方法改进为更强的属性。不能用所有（三个）工具验证的示例不是测试套件的一部分，这可能会使测试产生偏差最初的测试套件由127个测试组成5.3.1无效属性NBAC没有内置的对发现属性无效的支持。一个工具NBAC2LUCKY将很快公开提供给符号模拟器Lucky [16]，以帮助寻找反例。归纳法对于无效属性是完备的，所以Luke和Rantanplan都能找到无效属性的最短反例Luke在使用较长反例的无效属性上优于Rantanplan，如图4所示。图中的测试有2到7个步骤的反例卢克NBAC兰坦普兰累计完成率0.00.20.40.60.81.0A. Franzén/Electronic Notes in Theoretical Computer Science 144（2006）19311001010.10.1 10 100卢克见图4。Luke和Rantanplan在具有越来越长反例的1010.10.1110兰坦普兰图五. Rantanplan和MATH SAT3.2.1之间的执行时间比较（秒）5.4与MATH SAT比较由于有几个非常先进的SMT求解器可用，这将是互，使一个比较，至少其中之一。因此，Rantanplan中添加了一个功能，允许该工具以MATHSAT格式。 创建的公式是基本案例和步骤案例需要核实相关财产这些公式已经用MATH SAT3.2.1版，结果概述见图五、散点图中的每个点分别是Rantanplan和MATH SAT的一对执行时间。MATH SAT的执行时间是Rantanplan为了验证属性而求解的所有基本和步骤案例的总执行时间为什么这里描述的这种简单的程序有时具有更好的性能的可能解释是MathSAT不是增量决策程序，因此“兰坦普兰MathSAT32A. Franzén/Electronic Notes in Theoretical Computer Science 144（2006）196结论和今后的工作我们已经看到，一个增量SMT过程可以用非常简单的方法构造，并且与其他方法相比，仍然可以很好地执行Lustre程序的归纳验证有一类问题与较大的线性整数光泽表达式，我们的方法显然优于其他方法。与其他SMT决策程序相比，这里描述的程序不是很先进。其表现仍然与NBAC和Luke相当，这可以归因于三个关键领域的特别关注。第一个是从光泽到逻辑的转换能够只考虑每个SAT模型的相关约束，这使得该工具的性能得到了巨大的提升。其次是启发式发现的原因不满意的约束问题。通常有几个原因可供选择，并且它们修剪搜索空间的能力变化很大。最后，检测不满足约束问题的不完整过程使其更加有效。有几个改进，可以预期，以进一步提高这些都是早期修剪，这是检查部分命题真值分配的满足性。 对于诸如线性算法之类的情况，这可能是昂贵的，使用不完整的过程来捕获大多数可用的约束问题，从而削弱了早期修剪。另一个经常使用的想法是对约束进行预处理，试图在搜索开始之前发现不满意的约束组合这些和其他最近的创新成功地用于其他SMT程序，并且可以预期在这里也是有益引用[1] C. Barrett和S. Berezin CVC Lite：一种新的协作有效性实现。 在proc CAV'04，LNCS第3114卷。Springer，2004.[2] P. Bjesse和K.克莱森无状态空间变换的在FMCAD 2000会议记录，2000年。[3] M.博扎诺河Bruttomesso，A. Cimatti，T. Junttila，P. Rossum，S. Schulz和R.阿提亚尼线性算术逻辑的可满足性的增量和分层过程。在Proc.TACAS[4] M. D. Bvre. 在道尔顿的滑雪道上。1960年，达戈·幸运[5] J. W.中国佬在不可行线性规划中寻找有用的约束子集。INFORMS Journal on Computing，9（2）：164[6] J. W. Chinneck和E. W.德拉夫尼克线性规划中最小不可行约束集的定位。ORSA Journal onComputing，3（2）：157A. Franzén/Electronic Notes in Theoretical Computer Science 144（2006）1933[7] D. Deharbe和S.瑞妮丝轻量级定理证明的代码的单位 在procSEFM'03。IEEE ComputerSociety Press，2003.[8] G. 德尔赞诺自动 验证 的 参数化 缓存一致性协议。在CAV 2000的程序，2000年。[9] N. En和N.斯伦森可扩展的SAT求解器。第六届国际会议的理论和应用的满意度测试，2003年。[10] N. En和N.斯伦森 通过增量SAT求解的时间归纳。 第一届国际有界模型检验研讨会论文集，2003年。[11] A. 我来了Lustre程序的归纳验证的组合SAT求解和整数规划硕士[12] H. Ganzinger，G.哈根河Nieuwenhuis，A. Oliveras，和C.蒂内利DPLL（T）：快速决策程序。2004年7月，在美国波士顿举行的第16届计算机辅助验证国际会议（CAV）上[13] O. Guieu和J. W.中国佬分析不可行的混合线性规划INFORMS Journal on Computing，11（1）：63[14] N. Halbwachs，P.Caspi，P.Raymond和D.皮劳同步数据流程序设计语言Lustre.Proceedingsof the IEEE，79（9）：1305[15] N. Halbwachs和P. Raymond。一杯Lustre。2002年。[16] E.贾斯珀和P.雷蒙德。幸运语言参考手册。技术报告TR- 2004-6，Verimag。[17] B.珍妮特 线性关系分析中的动态划分。适用于核查同步程序。系统设计中的形式化方法，23（1）：5[18] M. Shepherd，S. Singh和G. Stalmarc k.使用感应和SAT解算器的安全特性。在计算机科学讲义，卷1954。Springer Verlag，2000年。[19] H. M. Sheini和K. A.萨卡拉一种基于SAT的混合逻辑/非线性问题的决策方法在计算机科学讲义中，第3524卷，第320-335页
我的内容管理
展开
