理论计算机科学电子笔记133（2005）119-137www.elsevier.com/locate/entcs混合系统有Martin Fréanzle1，3信息学和数学建模，丹麦技术大学林比Christian Herde克里斯蒂安·赫尔德2，3D epartmetofC omputingSience，C arl-von-O sietzkyU iv ersitauto ldenbur g，P. O. Box2503，D-26111 Oldenburg，Germany摘要在本文中，我们提出了HySat，一个新的有界模型检查的线性混合系统，incorporating一个紧密集成的基于DPLL的与MathSAT，ICS或CVC等相关工具相比，我们的工具利用了所有在有界模型检查上下文中自然出现的各种优化，例如，学习的冲突子句或定制的决策策略的同构复制，并将其扩展到混合域。我们证明，这些优化是至关重要的工具的性能。关键词：验证，有界模型检查，混合系统，无限状态系统，决策过程，满意度。1介绍在过去的十年中，数字系统的正式验证已经从一个学术课题发展成为一种被业界接受的方法，1 电子邮件地址：mf@imm.dtu.dk2电邮地址：christian. informatik.uni-oldenburg.de3这项工作得到了德国研究委员会（DFG）的部分支持，跨区域合作研究中心“复杂系统的自动验证和分析”（SFB/TR 14 AVACS）。如需详细信息，请参阅www.avacs.org1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.08.061120M. Fränzle角Herde/Electronic Notes in Theoretical Computer Science 133（2005）119现在有几十种商业工具可供各大公司使用在离散系统的形式验证中，最成功的方法之一是有界模型检验（BMC），如Groote等人在[17]和Biere等人在[9]中所建议的。 BMC的思想是将系统的下一状态关系编码由于近年来命题SAT检查器的性能取得了令人印象深刻的进步，BMC现在甚至可以成功地应用于非常大的有限状态设计。虽然最初仅针对离散过渡系统制定，但BMC的基本思想将对错误路径的搜索减少到公式的可满足性问题，也适用于混合然而，BMC公式所产生的这种系统不再是纯粹的命题，但通常包括复杂的布尔组合的算术约束的实值变量，从而需要新的决策程序来解决它们。我们的工具HySat提供了一个决策程序，该程序是为满足BMC对具有分段线性变量更新的无限例如线性混合自动机。HySat紧密集成了最将SAT的算法与用于数值约束的连接的决策过程相结合以求解其任意布尔组合的想法已经由几个组追求。 Wolfman和Weld首次提出了基于分辨率的SAT检查器与线性规划的紧密集成，并成功应用于规划问题[30]。 最近，Audemard等人[3]跟进了MathSAT，这是一种将SAT求解与Bellman-Ford算法（用于差分逻辑约束）和单纯形算法（用于一般线性约束）相结合的工具，用于时间推理和时间自动机模型检查的应用。支持更一般的公式类的工具是CVC[6]和ICS [15]，两者都集成了各种理论的决策过程，包括布尔逻辑，线性实数算术，未解释的函数符号，函数数组和抽象数据类型。然而，除了HySat之外，上述所有工具都缺乏在有界模型检查中自然出现的某些或所有特定优化-M. Fränzle角Herde/Electronic Notes in Theoretical Computer Science 133（2005）119121背景。如Shtrichman [26]所观察到的，BMC产生高度对称的SAT实例，因为它们包括系统转换关系的k这种特殊的结构可以用来加速求解，例如，通过将SAT求解器执行回溯搜索期间遇到的冲突的解释复制到所有同构部分为了从搜索树中修剪相似的冲突。这种技术在下文中被称为同构推断，已被证明在用比例SAT引擎执行BMC时产生相当大的性能增益。据我们所知，HySat是第一个将同构推理扩展到交叉转换的求解器，以及[ 26 ]中描述的其他特定于域的我们将证明，与纯粹的命题BMC相比，在这种情况下可以实现类似甚至更高的性能增益。原因是混合域中的推理步骤在计算上比命题逻辑中昂贵得多，因为现在必须处理更丰富的逻辑本文的结构如下。在下面的两个部分中，我们解释了我们的SAT检查器解决的逻辑语言，并简要回顾了如何将线性混合自动机转换为适用于有界模型检查的预测公式。在第4节中，我们详细解释了HySat的算法成分。特别是，我们讨论了在我们的工具中实现的特定于在第5节中，我们报告了一些实验结果，第6节得出结论，并描述了未来的研究方向。2的逻辑由于我们的目标是在没有先验有限状态抽象的情况下对线性混合自动机进行自动状态探索分析[20，19]， HySat解决了包含布尔值和实值变量的两种排序逻辑中的满意度问题在对线性混合自动机的性质进行编码时，布尔变量用于对离散状态分量进行编码，而实变量用于对连续状态分量进行编码。这些公式实际上是命题的，是布尔部分的线性零一约束[16]（也称为伪布尔约束[7]）和实值部分的保护线性约束[30formula：：={clause}子句子句：：=线性ZO约束|booleanvar = 0线性约束这里，线性约束表示实值变量上的线性不等式的合取，即任意线性规划的约束部分，而线性ZO约束表示布尔值变量上的线性不等式。使用线性0 - 1约束子句而不是例如，122M. Fränzle角Herde/Electronic Notes in Theoretical Computer Science 133（2005）119析取子句（如合取范式）的一个重要原因是线性0 - 1约束比析取子句更简洁，并且我们有一个非常有效的SAT求解器-称为2.1零一线性约束将任意命题公式改写为合取范式（CNF），在保持命题变量个数不变的情况下，公式的规模将出现最坏情况下的指数爆破为了避免这种情况，所有实际的验证环境都利用了满足性保持变换，通过引入线性数量的辅助变量[27，25，28]来产生线性大小的编码。然而，引入线性数量的辅助变量的代价是，在回溯搜索时搜索树的大小的最坏情况下的指数爆炸。然而，人们已经观察到，这两个原因的爆破往往可以避免，作为戴维斯-普特南-Loveland-Logemann搜索过程，以满足赋值顺利推广到零-一线性约束系统（ZOLCS），这是零-一线性规划的约束部分[7，29，2，16]。零-一线性约束系统的表达能力足以促进线性大小编码，例如，门级网表，而不使用辅助变量。在零-一线性约束系统或线性伪布尔约束系统中，公式是线性零-一约束的合取。线性0 - 1约束的形式为a1x1+ a2x2+. anxn≥k，其中xi是文字，即正或负的命题变量，ai是自然数，称为各个文字的权重，k∈N是阈值给定命题变量的布尔赋值，当文字的真值false和true分别用0和1标识时，如果零-一约束的左侧求值为超过阈值的值，则零-一约束被满足。 0 - 1约束可以表示一类单调布尔函数，例如，1a + 1b + 1c + 1d≥ 1等价于abcd，1a + 1b +1c + 1d≥ 4等价于abcd，1a + 1b + 3c + 1d≥ 3等价于c=（abd）。因此，ZOLCSc_n基本上比C_N更重要。F：请注意，k个变量中有n个应该为真，n 长度为neachh，即 我是O。. 恩纳克K n，而相应的ZOLCS具有尺寸线性k和n的对数。形式上，线性0 - 1约束的语法是M. Fränzle角Herde/Electronic Notes in Theoretical Computer Science 133（2005）119123B线性ZO约束：：=线性项≥阈值线性项：：={weight literal+}{weight literalweight：：∈Nliteral：：= boolean var| booleanvarboolean var：：∈BVthreshold：：∈N其中BV是布尔变量名称的可数集合。Zeronecon stra reint表示命题变量的一个值σB：BV−to→talB。 σB满足约束条件a1x1+ a2x2+. anxn≥ ki a1xσB（x1）+a2xσB（x2）+. anxσB（xn）≥k，其中⎧且σB（x）=false，χσB（x）=⎪ 1如果x∈V且σB（x）=真，<$1 −χσB（y）如果x<$y对于某个y ∈V。2.2保护线性约束零一约束只能表示布尔变量上的约束第二类子句是布尔保护线性约束，它表示实值变量之间的（线性）约束，以及它们与布尔赋值的相互依赖性。一个受保护的线性约束仅仅是一个蕴涵boolean var=0线性约束布尔变量和实值变量上的线性约束之间的关系，即一个线性不等式的合取这样的受保护的线性约束是对一个V值方程σ=（σB，σR）∈（BV−to→talB）×（RV−to→talR）进行了解释，其中RV是在线性约束中出现的实变量的集合。保护线性约束v=σc满足σ=（σB，σR）iσR满足线性约束c或如果σB（v）=false。2.3满足公式公式φ是线性0 - 1约束和保护线性约束的合取，因此可以在赋值总σ=（σB，σR）∈（BV−→）×（RV−to→talR）。显然，φ满足σ =（σB，σR），记为σ| = φ，i φ中的所有线性0 - 1约束都由σB满足，φ中的所有保护线性约束都是124M. Fränzle角Herde/Electronic Notes in Theoretical Computer Science 133（2005）1192X505 10 15 20吨Fig. 1.线性混合自动机和样本轨迹。l x和u x表示x在相应状态下斜率的上下限，而x≤10和x≥4是约束x本身的状态不变量。满足（σB，σR）。当用类似Davis-Putnam的程序解决公式的可满足性问题时，我们将逐步建立估值，这样我们就必须推理关于部分赋值ρ∈（BV部分−→B）×（RV部分- →R）的变量。 我们说变量v∈ BV<$RV在ρi <$v/∈dom（ρB）<$dom（ρR）中是未赋值的。对于公式φi，部分赋值ρ称为相容的，其中存在一个总数扩展σ：（BV−to→talB）×（RV−to→talR）ofρ满足φ。其他的，我们称ρ对φ不一致。 此外，称一个部分赋值ρ满足φi，且它的所有扩张都满足φ。由于这个满意度的定义与前一个关于总估值的定义一致，我们将使用相同的符号ρ |= φ表示部分和全部估值的满足。3线性混合自动机如图1所示，线性混合自动机A=（k，T，R，inv，l，u，m，g，ass，init）包括：• a finite有限set组numerals地点，• 一个有限的转换集T，• 连续状态分量的有限集合R• 一族状态不变量inv=（invσ）σ∈n，其中每个状态不变量invσ是R上的线性谓词，当控制位于离散位置σ时，它约束连续状态分量的赋值，• 两个族l=（lσ，x）σ∈N，x∈R和u=（uσ，x）σ∈N，x∈R，当控制驻留在位置σ时，为每个位置σ∈N和每个连续状态分量x∈R分配x的最小和最大斜率。个人lσ，x是Q<${−∞}中的常数，同样uσ，x∈Q <${∞}。• 映射m：总T−→ T →T为每个跃迁分配一对源和转换的sink状态• 族g=（gt）t∈T，为每个转移分配使能该转移的转移保护，其中转移保护是R上的线性谓词，四、5
下载后可阅读完整内容，剩余1页未读，立即下载
