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

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.

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

对于一些安全攸关系统，必须借助于形式化方法才能保证其正确性和可靠性。作为最成功的形式化验证方法之一，模型检测技术在工业界（尤其是硬件界）得到了广泛的应用。本课题针对模型检测的状态空间爆炸问题，研究将归纳不变式应用到模型检测技术之中。首先，提出了一种基于学习的归纳不变式生成方法；其次，基于归纳不变式实现了一种面向安全属性的验证方法；再次，系统全面的研究了基于学习的组合验证方法，并将其扩展到概率系统与回归验证。最后，基于上述成果，开发了模型检测工具Beagle和软件验证工具Ceagle，并在某航空发动机控制软件系统中进行应用。