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

项目名称： 基于假设/保证自动推理的组合验证研究

项目编号： No.60903030

项目类型： 青年科学基金项目

立项/批准年度： 2010

项目学科： 金属学与金属工艺

项目作者： 贺飞

作者单位： 清华大学

项目金额： 17万元

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

中文关键词： 模型检测；组合验证；假设/保证推理；可满足性判定；嵌入式系统

英文摘要：

英文关键词： model checking；compositional verification；assume/guarantee reasoning；satisfiability；embedded systems