基于归纳不变式的带参协议验证

Parameterized protocol verification is important but hard in the frontier research field of formal methods, progress has been slow in recent years. The main difficulties lie in: automatic construction of auxiliary inductive invariant set, the rigor of the theoretical basis of the method itself, and the scale of protocol which can be handled. Basing on the latest result of the theory and methods in the field of interactive/automatic theorem proving, this project tries to better address the above-mentioned difficulties in the art. The main contents include: 1) the establishment of appropriately formal semantic model used to describe the semantics of behavior and goal of a parameterized protocol; 2) newly inductive proof method for parameterized protocol verification; 3) new method to automatically construct inductive invariants; 4) construction of a unified framework to combine computing inductive invariant set with proof generation and proof checking; 5) case studies such as cache coherency protocol, high-speed rail train control protocols. The results are not only expected to have a positive impact in the theory, but also will also promote the development of technology and tools to solve practical problems in some areas of high-end manufacturing.

带参协议验证是形式化方法领域重要的前沿难题,近年来进展缓慢，难点主要集中在：辅助归纳不变式集合的自动构造，验证方法本身理论基础的严格性，以及所能处理的协议的规模。本项目将基于最新的交互式/自动定理证明理论与方法，对带参协议验证进行深入的研究，更好地解决本领域的上述难点。主要内容包括：1)建立适合带参协议系统描述的语义模型，以用于描述带参协议的语义行为与协议性质。2)提出新的基于归纳证明的带参协议系统验证方法。3)提出新的方法自动构造归纳证明需要的不变式。4)构造新的验证框架，融合归纳不变式集的计算，带参协议系统的证明的自动构造，证明的检测。5)对典型的带参协议系统如缓存一致性协议，高铁列控协议等进行实例研究。其预期成果不但对带参协议验证领域的理论产生积极影响，而且也将推动相应的技术工具集的发展，从而解决高端制造领域若干现实问题。

带参协议验证是形式化方法领域重要的前沿难题,近年来进展缓慢，难点主要集中在：辅.助归纳不变式集合的自动构造，验证方法本身理论基础的严格性，以及所能处理的协议的规模.。本项目将基于最新的交互式/自动定理证明理论与方法，对带参协议验证进行深入的研究，.针对本领域的难点，本项目将主要内容包括：.a).建立了基于卫士选择(guarded choice)的带参协议的语义模型的研究；.b).基于三种证明依赖关系的，针对带参协议的归纳证明方法的研究;.c).基于三种证明依赖关系的带参证明构造，以及结合模型检测技术、机器学习技术的归纳.不变式的自动构造的研究；.d).基于paraVerifier的客户端/服务器带参协议验证框架的实现，以及验证工具的实现与.集成以及在缓存一致性协议验证中的应用。 .其成果不但对带参协议验证领域的理论产生积极影响，而且推动了相应的技术工具集的发展，得到国际同行的认可。