论文标题
矩形混合系统的模型检查：一种量化的编码方法
Model Checking for Rectangular Hybrid Systems: A Quantified Encoding Approach
论文作者
论文摘要
可满足的模量理论（SMT）求解器已成功地用于解决正式验证中的许多问题，例如有限模型检查（BMC），从集成电路到网络物理系统，许多类别的系统。通常，BMC是通过检查可能长但无量词公式的满意度来执行的。但是，在BMC步骤的数量上，可以自然地将BMC问题编码为量化公式。然后，我们使用支持量化器的决策程序来检查这些量化公式的满意度。此方法先前已应用于使用纯离散系统编码的量化布尔公式（QBF）执行BMC，然后使用QBF求解器放电QBF检查。在本文中，我们为矩形混合自动机（RHA）提出了BMC的新量化编码，该编码需要由于真实的（密度）时间和现实价值的状态变量建模连续状态而使用更一般的逻辑。我们使用HYST模型转换工具实现了该方法的初步实验原型，以生成Z3 SMT求解器的量化BMC（QBMC）查询。我们描述了几种定时和混合自动机基测试基准的实验结果，例如Fischer和Lynch-Shavit相互排斥算法。我们比较了无量词BMC方法的方法，例如使用DREAL SMT求解器的Dreach工具中的方法，以及使用Mathsat SMT求解器的NuxMV顶部构建的HYCOMP工具。基于我们有希望的实验结果，QBMC将来可能是RHA和其他类别的混合自动机的有效分析方法，因为SMT求解器（例如Z3）中的量化器处理中会进一步改进。
Satisfiability Modulo Theories (SMT) solvers have been successfully applied to solve many problems in formal verification such as bounded model checking (BMC) for many classes of systems from integrated circuits to cyber-physical systems. Typically, BMC is performed by checking satisfiability of a possibly long, but quantifier-free formula. However, BMC problems can naturally be encoded as quantified formulas over the number of BMC steps. In this approach, we then use decision procedures supporting quantifiers to check satisfiability of these quantified formulas. This approach has previously been applied to perform BMC using a Quantified Boolean Formula (QBF) encoding for purely discrete systems, and then discharges the QBF checks using QBF solvers. In this paper, we present a new quantified encoding of BMC for rectangular hybrid automata (RHA), which requires using more general logics due to the real (dense) time and real-valued state variables modeling continuous states. We have implemented a preliminary experimental prototype of the method using the HyST model transformation tool to generate the quantified BMC (QBMC) queries for the Z3 SMT solver. We describe experimental results on several timed and hybrid automata benchmarks, such as the Fischer and Lynch-Shavit mutual exclusion algorithms. We compare our approach to quantifier-free BMC approaches, such as those in the dReach tool that uses the dReal SMT solver, and the HyComp tool built on top of nuXmv that uses the MathSAT SMT solver. Based on our promising experimental results, QBMC may in the future be an effective and scalable analysis approach for RHA and other classes of hybrid automata as further improvements are made in quantifier handling in SMT solvers such as Z3.
