针对软件验证大规模化问题，设计可复用验证基础设施、提高验证自动化水平是解决途径。构造规范多层次精化模型可以消除语义断层，以一阶逻辑和集合论描述的多层次精化模型将作为可复用验证基础设施。计算机代数系统Mathematica支持一阶逻辑和集合论，集成了大量数学算法，复用它们可以提高验证自动化水平。本项目研究模块规范建模以及精化模型与模块代码之间精化验证方法。基于Event-B方法和Mathematica语言，拟解决关键问题包括:如何丰富Event-B方法建模工具的建模语言并提升证明义务验证能力?如何构造精化不变式?如何实现验证工具?本项目将基于Mathematica语言和Event-B建模方法构造模块规范多层次精化模型,基于精化策略和随机测试等方法发现精化不变式,基于Mathematica语言实现验证工具。在上述研究基础上,将验证工具应用于操作系统模块和TLS协议程序模块验证。

Designing the reusable verification infrastructure and enhancing the automatic level of verification are the main ways for verifying scalable software. For software verification, the semantic gap between the specification and the codes is the hard problem, constructing multiple-layer refinement models is an effective way to tackle the semantic gap, the multiple-layer refinement models described based on the first-order logic and set theory will be the reusable verification infrastructure. The computer algebra system Mathematica supports the first-order logic and set theory, integrates plenty of mathematic algorithms, reusing these algorithms will enhance the automatic level of software verification. The main contents of this research are focused on the modeling of the software modular specification and the automatic or semi-automatic refinement verification between refinement model and the modular code. Based on the Event-B method and Mathematica, the key problems to be solved in this research consist of: how to enrich the modeling language and improve the proof abilities of proof obligations for Event-B’s modeling tool? Based on the multiple-layer refinement models, how to construct the refinement invariants? And how to design and develop a support tool? In this research, the Event-B modeling method and the Mathematica language will be combined to construct the multiple-layer refinement models, the refinement invariants will be discovered from the multiple-layer refinement models with refinement tactics and random testing, also from codes by constructing equality loop invariants. The support tool will be designed and developed based on Mathematica. Based on the above researches, the support tool will be utilized further to verify the modular codes of the operational system and the TLS security protocol.