基于自动机技术的符号模型检验

理论计算机科学电子笔记150（2006）3-8www.elsevier.com/locate/entcs基于自动机技术的符号模型检验邀请地址Axel Legay1，3Pierre Wolper2Institut MonteFioreUniversit′edeLi`ege，Li`ege，Belgium摘要在有限状态系统中的检查通常是通过将有限状态集编码为正则语言来完成的。计算这样一个规则的表示，比如说，一个系统的可达状态集需要加速技术，这种技术可以有限地计算无限数量的转换的结果。在已经提出的加速技术中，人们发现了特定和通用技术。特定的技术利用被分析的特定类型的系统，例如，操作队列或整数的系统，而一般技术仅假设转换关系由有限状态转换器表示，该转换器必须迭代。 在本文中，我们调查了[3]和[4]中提出的两种通用技术。这些技术建立在早期工作的基础上，但利用了许多新的概念和算法思想，这些思想通常是在实验的帮助下产生的，这使它具有广泛的范围和良好的性能。关键词：（ω−）正则模型检验，调查.在所有已经提出的用于探索有限状态空间的技术的核心，是一种可以有限地表示有限状态集在这个主题的早期工作中，这种表示是特定的，例如实向量集的线性约束几年来，基于通用有限自动机的表示可以在许多环境中使用的想法已经得到了发展，从系统操作开始1Email：legay@montef i ore. 尤尔湾梭Be2Email：pw@montefiore. 尤尔湾梭Be3 阿克塞尔·莱盖得到了F.R.I.A.的资助。1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.12.0204A. Legay，P.Wolper/Electronic Notes in Theoretical Computer Science 150（2006）3lating队列和整数[8，11，9，13]，然后移动到参数系统[6]，最近，到达使用实变量的系统[10，2]。为了探索无限状态空间，不仅需要无限集合的有限表示，还需要有限计算无限数量转换的效果的技术这些技术可以是领域专用的或通用的。域特定技术利用所考虑的域的特定属性和表示，例如，在[15，14]中获得队列，在[17，22，12]中获得整数和实数，在[18，16]中获得下推系统，在[19]中获得有损信道通用技术考虑有限自动机表示，并提供直接在此表示上操作的算法，大多数情况下忽略它所使用的域类属技术最早出现在系统验证的背景下，这些系统的状态可以用有限个词编码，比如参数系统。这里使用的思想是，一个配置是一个有限词，一个转换关系是一个有限词上的关系，或者等价地是一个有限词对的语言。如果这种语言是正则的，它可以用有限状态自动机来表示，更具体地说，是一个有限状态转换器，然后问题就变成了迭代这样一个转换器。有限状态转换器非常强大（图灵机的转换关系可以用有限状态转换器来建模），硬币的另一面是这样一个转换器的迭代既不总是可计算的，也不规则。然而，有许多实际相关的情况下，有限状态换能器的迭代可以计算并保持有限状态。识别这种情况并开发迭代有限状态transduc- ers的（部分）算法一直是最近一系列论文的主题，称为启动本演讲中提出的工作[3]的问题是，迭代换能器的通用技术是否可以有效地应用于迄今为止专门使用特定领域技术特别是，我们的目标之一是将表示算术关系的有限状态转换器（参见[22]的调查）。除了单纯的好奇心之外，动机是能够解释不符合特定领域结果所需形式的关系最初的结果非常令人失望：像（x，x+ 1）这样简单的算术关系的转换器不能通过现有的然而，通过实验和理论工作的混合来寻找这种不可能性的根源，并采取务实的方法来解决发现的问题，我们能够开发出一种迭代传感器的方法，可以轻松处理算术关系，以及许多其他情况。有趣的是，它是通过使用一种操纵自动机的工具（LASH [24]），观察前A. Legay，P.Wolper/Electronic Notes in Theoretical Computer Science 150（2006）35样本超出了手动模拟的范围，并测试了各种算法，正确的直觉，后来被理论论证验证，被开发出来。因此，实施不是事后的想法，而是我们研究过程的核心已经采取的一般方法类似于[21]中的方法，在这个意义上，从换能器T开始，我们计算T的功率Ti，并试图推广所获得的换能器序列，以捕获其无限并集。这是通过比较T的连续幂并尝试将T的幂之间的差异表征为添加的一组状态和转换来完成的。如果这组添加的状态或增量总是相同的，则可以将其插入到循环中以捕获T的所有幂。然而，对于比较Ti和Ti+1的算术传感器，没有产生任何增加的存储容量，尽管在T2中使用T2i+1是的。因此，我们使用d不是为了比较Ti和Ti+1，而是为了从换能器的功率序列中提取样本序列，并使用该样本序列进行工作给定用于表示算术关系的二进制编码，在这种情况下，以2的幂进行采样工作得很好，但是采样方法是通用的并且是不同的样本序列可以将其存储在存储器4中。 现在，如果我们完全符合RSamp LEPWERTik传感器和计算这不需要一个完整的设备，K我计算iT。幸运的是，这个问题很容易解决，响应变换器，即T0=T<$TI，其中TI是单位变换器，这种情况下使用无限子序列的样本是足够的。一旦序列中的自动机被构造和比较，并且对应于连续元素之间的差异的增量已经被识别，下一步是通过将其合并到循环中来允许该关于如何做到这一点有一些技术问题，但没有重大困难。一旦获得了所得到的外推法安全的一个容易检查的充分条件是，它与自身组合时保持不变检查精确性是更微妙的，但我们已经制定了一个程序，体现了一个足够的标准这样做其思想是检查具有给定数量k个增量副本的换能器的任何行为可以通过组合具有少于k个增量副本的换能器来获得这是通过用计数器增加待检查的换能器并证明可以将这些计数器限制在有限范围内来完成的，因此允许使用有限状态技术。4作为一个例子，它往往是线性时，考虑参数系统6A. Legay，P.Wolper/Electronic Notes in Theoretical Computer Science 150（2006）3利用这一事实，我们的外推技术的自动机上工作，而不仅仅是传感器，我们考虑计算可达的状态都通过计算封闭的传感器代表的过渡关系，并通过重复应用的传感器的一组初始状态。第一种方法产生了一个更一般的对象，并且如果希望将该方法扩展到活性属性的验证（[1，25]），则是必不可少的当使用状态集而不是转换器工作时，并不总是可以检查精确度，但是这仅仅相当于说所计算的可能是可达状态集的过近似，已知这种情况在实用上是没有问题的。更进一步，使用常规的模型检测技术的问题，其状态是由无限（Ω）字表示的系统已经解决。这使得实数集的表示成为可能，如[2，12]所述 为了避免在无限词自动机上实现某些操作所需的算法的困难，只考虑了可以由确定性的Bu？hi自动机[7]定义的ω-正则集。这是一个严格的过程，但如[2]所示，处理线性约束的一阶理论中定义的实数集是足够此外，使用这样的表示导致算法与有限词情况下使用的算法非常相似，并允许我们将简化的确定性自动机作为范式进行工作。 由于这些优点和性质，人们可以证明，为有限词格开发的技术可以直接适用于弱确定性的Bu？hi自动机，直到算法的定义[4]。我们的技术已经实现了一个原型，部分依赖于LASH包。这个原型已经过测试的几个案例研究来自不同的视野。在我们的实验中，我们能够模拟各种算术（整数或实数）传感器。我们还成功地处理了早期特定技术（如[17，12]）无法处理的析取关系该技术也成功地应用于参数系统的例子和Petri网的分析。此外，混合系统的模型，包括泄漏的气体燃烧器和交替位协议与定时器也被考虑。试图在有限状态系统中进行验证，同时只使用自动机理论表示和算法，这似乎有点不切实际。然而，实际结果清楚地表明了他们的兴趣，因此是新发展的动力[27，26，28]。A. Legay，P.Wolper/Electronic Notes in Theoretical Computer Science 150（2006）37引用[1] A. Bouajjani和B. Jonsson和M. Nilsson和Tayssir Touili，Regular Model Checking，Proceedingsof the 12th International Conference on Computer-Aided Verification（CAV[2] B. Boigelot和S. Jodogne和P. Wolper，关于使用弱自动机来决定具有实数和实数变量的线性算术，Proc. International Joint Conference on Automated Reasoning（IJCAR），计算机科学讲义，第2083卷，200年，第611- 625页。[3] B. Boigelot和A. Legay和P. Wolper，大型迭代传感器，Proc.15th Int. Conf. on ComputerAided Verification，Boulder，USA，计算机科学讲义，第2725卷，2003年，第223[4] B. Boigelot和A. Legay和P. Wolper，Omega-Regular Model Checking，Proc.10th Int. Conf. onTools and and Algorithms for the Construction and Analysis of Systems，Barcelona，Spain，Lecture Notes in Computer Science，2988卷，2004年，第561-575页。[5] D. Dams 和 Y. Lakhnech 和 M. Ste Escheren ， Iterating Transducers ， Proceedings 13thInternational Conference on Computer Aided Verification（CAV），Lecture Notes in ComputerScience，2001年第2102卷，第286[6] Y. Kesten和O. Maler和M. Marcus和A. Pnueli和E. Shahar，Symbolic Model Checking with RichAssertional Languages ， Proceedings of 9th International Conference on Computer- AidedVerification（CAV[7] D. E. Muller和A. Saoudi和P.E.李文，《自动机理论与应用》，北京大学出版社，1986年。[8] P. Wolper 和 B. Boigelot ， Presburger 算 术 约 束 的 自 动 机 理 论 方 法 ， Proc. Static AnalysisSymposium，Glasgow，Lecture Notes in Computer Science，卷983，1995年，21-32。[9] P. Wolper和B. Boigelot，具有无限但规则状态空间的系统，Proc.10th Int. Conf. on ComputerAided Verification，Vancouver，Lecture Notes in Computer Science，1427卷，1998年，88-97。[10] B. Boigelot和L. Bronne和S.李文，强线性混杂系统的可达性分析方法，第九届国际计算机辅助验证大会论文集，北京，计算机科学出版社，1997年，第167-177页。[11] B. Boigelot和P. Godefroid和B. Willems和P.Wolper，量子点的力量，Proc.of Int. Static AnalysisSymposium，Paris，Lecture Notes in Computer Science，1302卷，1997年，第172-186页。[12] B. Boigelot和F. Herbreteau和S. Jodogne，Hybrid Acceleration Using Real Vector Automata，Proc.15th Int. Conf. on Computer Aided Verification ， Boulder ， Lecture Notes in ComputerScience，volume2725，year 2003，193-205.[13] B. Boigelot和S. Rassart和P. Wolper，论实数算术自动机的表达性，Proc.25th ICALP，计算机科学讲义，1443卷，1998年，152-163。[14] A. Bouajjani和P. Habermehl，Symbolic Reachability analysis of FIFO channel systems withnonregular sets of configurations，Proc.24th ICALP，Bologna，Lecture Notes in ComputerScience，1256卷，1997年，560-570。[15] B. Boigelot和P. Godefroid，使用QDD对具有无限状态空间的通信协议进行符号验证，Proc.8thInt. Conf. on Computer Aided Verification，New Brunswick，计算机科学讲义，第1102卷，1996年，1-12。[16] A. Bouajjani和J. Esparza和O. Maler，下推自动机的可达性分析：在模型检查中的应用，Proc.8thInt. Conf. of Concurrency Theory，Warsaw，Lecture Notes in Computer Science，1243卷，1997年，135-150。8A. Legay，P.Wolper/Electronic Notes in Theoretical Computer Science 150（2006）3[17] B. Boigelot ， Symbolic Methods for Exploring Infinite State Spaces ， Collection desPublicationsdelalaFacult′eddesSciencessApp liqu′eesd el' U ni v e rsit ′ ed e L i `ege ，L i `ege，Belgi um m，y e a r 1999.[18] A. Finkel和B. Willems和P. Wolper，模型检测下推系统，Proc 2th Int.无限状态系统验证研讨会，博洛尼亚，理论计算机科学电子笔记，第9卷，1997年[19] P.A. Abdulla和B.Jonsson，《具有不可靠通道的程序，信息和计算》，卷127（2），1996年，第91-101页[20] B. Jonsson和M. Nilson，Transitive closure of regular relations for verification in finite-statesystems ， Proc 6th Int. Conf. on Tools and Algorithms for the Construction and Analysis ofSystems，Lecture Notes in Computer Science，1875卷，2000年，第220-234页。[21] T. Touili，使用加宽技术进行常规模型检查，Proc 1st。参数化系统验证研讨会，理论计算机科学电子笔记，2001年。[22] B. Boigelot 和 P. Wolper ， 用 有 限 自 动 机 表 示 算 术 约 束 ： 概 述 ， Proc. Int. Conf. on LogicProgramming，哥本哈根，计算机科学讲义，第2401卷，2002年，1[23] P. A. Abdulla和B. Jonsson和M. Nilsson和J.[24] Li`egAut omata-basedSymbolicH and ler（LASH）. Availab leathttp://www.montefiore.ulg.ac.be/搜索{}boigelot/research/lash/。[25] A. Bouajjani和A.Legay和P.Wolper，Handling Liveness properties in（ω-）Regular ModelChecking，出现在ENTCS中。[26] P. A. Abdulla和A. Legay和J. D'Orso和A. Rezine，基于仿真的树型传感器迭代，Proc. 11 th Int.Conf. on Tools and Algorithms for the Construction and Analysis of Systems，Edinburgh，U-K，计算机科学讲义，第3440卷，2005年，第30-44页。[27] A. Bouajjani和P. Habermehl和P. Moro和T. Vojnar，在常规模型检查中使用动态1-选择器链接结构 的 并 行 程 序 ， Proc.11th Int. Conf. on Tools and and Algorithms for the Construction andAnalysis of Systems，Edinburgh，U-K，计算机科学讲义，第3440卷，2005年，第13-29页。[28] A. Vardan和K. Sen和M. Viswanathan和G. Agha，Using Language Inference to Verify Omega-Regular Properties ， Proc.11th Int. Conf. on Tools and Algorithms for the Construction andAnalysis of Systems，Edinburgh，U-K，Lecture Notes in Computer Science，volume3440，year 2005，pages 30-44.