基于混成计算的多核限界模型检测

Model checking has been broadly researched as an effective technique for improving software correctness. Recent years, software industry has begun to adopt model checking by applying it to practical software development process. However, existing model checking techniques and tools are still not able to accomplish verification of large-scale software systems. Focusing on bounded model checking (BMC), a technique that can manage relatively larger verification problems, this project proposes a novel hybrid-computation based multicore BMC technique to further enhance BMC’s verification capability and efficiency. In this technique, (stateless) explicit exploration algorithms are integrated into BMC: the former helps, through state space abstraction and execution path extraction, to compress and split encoded logical formulas and facilitate multicore computation with SMT solvers; the latter helps, with the support of unsat-core information from SMT solvers, to reduce the state space to be explicitly explored. The project refines five scientific problems that are critical for accomplishing this novel technique, and proposes practical solutions for each of them. Preliminary work has realized parts of this proposed technique, and experimental results (CompJ,2014) demonstrate that the partial implementation done so far has already achieved better performance than the well-known BMC tool SAL, and partly better than NuSMV. Successful promotion of this project is going to remarkably enhance BMC’s verification capability and efficiency, and contribute to large-scale software verification with theoretical and tool supports.

模型检测作为提高软件正确性的有效技术被广泛研究，并于近年开始实际应用于软件开发产业中。然而，现有技术和工具仍无法实现对大规模软件系统正确性的验证。本项目着眼于可处理较大规模验证问题的限界模型检测技术，为进一步提升其验证能力和性能，提出新型的基于混成计算的多核限界模型检测技术：将(无状态)显式探索算法融合于限界模型检测，前者通过抽象状态空间及抽取执行路径为后者压缩、拆分编码公式、实现多核验证；后者的SMT求解器提供不可满足核心为前者缩减需探索的状态空间。本项目凝练出实现该新型技术的5个关键科学问题，并逐一提出切实可行的研究方案。项目组在前期工作中已实现本项目的部分算法，实验结果表明(CompJ,2014)，该技术的现有验证能力和性能已优于知名限界模型检测工具SAL，部分优于NuSMV。本项目的成功实施，有望显著提升现有限界模型检测技术的性能，为实现大规模软件正确性验证提供理论和工具支撑。

模型检测作为提高软件正确性的有效技术被广泛研究，并于近年开始实际应用于软件开发产业中。然而，现有技术和工具仍无法实现对大规模软件系统正确性的验证。本项目着眼于可处理较大规模验证问题的限界模型检测技术，为进一步提升其验证能力和性能，提出新型的基于混成计算的多核限界模型检测技术：将（无状态）显式探索算法融合于限界模型检测，前者通过抽象状态空间及抽取执行路径为后者压缩、拆分编码公式、实现多核验证；后者的SMT求解器提供不可满足核心为前者缩减需探索的状态空间。该算法同时融入插值抽象方法，可进一步扩展为非限界模型验证。基于该算法，本项目发表学术论文14篇，其中CCF列表论文4篇，SCI论文5篇，EI论文14篇，培养软件工程及形式化验证领域青年教师3年，博士生3人，硕士生7人；另外，本项目基于该算法开发实现了模型检测工具Garakabu2。实验显示，Garakabu2的验证能力和性能已优于知名限界模型检测工具SAL且部分优于NuSMV（部分安全属性提升10倍以上），为实现大规模软件正确性验证提供了理论和工具支撑。