基于假设/保证自动推理的组合验证研究

状态空间爆炸问题是制约模型检测应用的主要问题。基于假设/保证（Assume/Guarantee，简称A/G）规则的自动推理框架被认为是最有前途的组合验证方法学之一，具有非常重要的理论与应用价值。区别于一般的A/G组合验证，该框架能够完全自动化。该技术的研究在国际上仍是崭新且富有挑战性的，有很多问题尚未解决。本课题拟对该技术的三个基本问题展开研究，即A/G自动推理框架、模型自动分解算法和符号化模型检测算法。此外，本课题还将从应用角度对该技术进行探讨，将基于接口自动机对该理论进行扩展，并将其应用到典型嵌入式系统的验证之中。

状态空间爆炸问题是制约模型检测应用的主要问题。基于假设/保证（Assume/Guarantee，简称A/G）规则的自动推理框架被认为是最有前途的组合验证方法学之一，具有非常重要的理论与应用价值。本课题对该技术的三个基本问题展开研究，即A/G自动推理框架、模型自动分解算法和符号化模型检测算法。主要研究内容包括：模型自动分解算法、A/G自动推理框架、基于其他自动机的扩展、符号化验证算法、符号化验证引擎等。本项目达到并部分超过了预期的目标，至今已发表学术论文8篇（包括IEEE Transactions on Computers 2篇，本领域顶级会议CAV 1篇）。设计并实现了一个面向构件化嵌入式系统的模型检测工具VCS，并且在门仓控制系统、多功能车辆总线控制器（MVBC）等典型嵌入式系统中进行了应用。