基于归纳不变式的模型检测研究

项目名称： 基于归纳不变式的模型检测研究

项目编号： No.61272001

项目类型： 面上项目

立项/批准年度： 2013

项目学科： 自动化技术、计算机技术

项目作者： 贺飞

作者单位： 清华大学

项目金额： 61万元

中文摘要： 对于一些安全攸关系统，必须借助于形式化方法才能保证其正确性和可靠性。作为最成功的形式化验证方法之一，模型检测技术在工业界（尤其是硬件界）得到了广泛的应用。将模型检测技术应用于软件系统验证，面临的最大问题是状态空间爆炸。基于归纳不变式的模型检测技术被认为是应对该问题的有效途径之一。该技术的研究在国际上仍是崭新且富有挑战性的，具有非常重要的理论与应用价值。本课题拟对该技术几个关键问题展开研究，包括：归纳不变式自动生成技术，基于归纳不变式的模型检测技术，和基于归纳不变式的组合验证技术。以此为基础设计支持复杂构件化系统的模型检测工具，并在典型嵌入式系统中进行应用。

中文关键词： 形式化方法；模型检测；归纳不变式；假设-保证推理；

英文摘要： Formal methods are needed for ensuring correctness of some safety-critical systems. Known as one of the most successful techniques in formal verification, model checking has been widely accepted in industry, especially in the hardware industry. State space explosion problem is the main obstacle for model checking in software systems. Inductive invariant-based model checking has been considered as a promising approach to this problem. This technique is still new and remains challenging. It is valuable both for theory and practice. This project addresses key issues in this technique, including: automatic generation of inductive invariants, inductive invariant-based model checking, and inductive invariant-based compositional verification. The project will develop a model checking tool which supports verification of large component-based systems. The research outcomes will be applied in some typical embedded systems.

英文关键词： formal methods；model checking；inductive invariants；assume-guarantee reasoning；