大规模软件验证若干关键技术研究及支持工具

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.

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

针对软件验证大规模化问题，设计可复用验证基础设施、提高验证自动化水平是解决途径。构造规范多层次精化模型可以消除语义断层，以一阶逻辑和集合论描述的多层次精化模型将作为可复用验证基础设施。计算机代数系统Mathematica支持一阶逻辑和集合论，集成了大量数学算法，复用它们可以提高验证自动化水平。本项目研究模块规范建模以及精化模型与模块代码之间精化验证方法。本项目的主要研究内容： (1)基于精化策略和随机测试提出了函数等式循环不变式的构造和验证方法，可以构造并验证最大公因数的算法程序、计算幂函数算法程序以及计算阶乘的算法程序等算法程序的函数等式循环不变式。 (2)基于Mathematica软件和抽象解释理论提出了约束优化问题的求解方法，能够计算出一些Mathematica软件无法求解的约束优化问题的最优解。 (3)基于Mathematica语言和Event-B方法设计并实现了建模与验证工具mathRodin,能够建模并验证飞机避让系统等出现实数类型和实函数的复杂系统。(4)调研了基于Event-B方法的安全协议建模与验证方法，基于Event-B方法为简化的Needham-Schroeder协议和改进的Needham-Schroeder协议建立了形式化模型。(5)基于Event-B方法和Event-B方法支持工具Rodin为MSI协议、MESI协议以及MOSEI协议等cache一致性协议建立了形式化模型，严格证明了这些cache一致性协议的正确性。(6)提出了大规模事务型verilog程序的抽象精化迭代验证方法，避免了模型检验大规模事务型verilog程序时的状态空间爆炸问题，并在工程实践中基于模型检验工具Jaspergold发现了私有化l2cache设计中的十几处设计bug。上述研究为基于Mathematica语言和Event-B方法建模并验证大规模软/硬件系统探索了可行途径。