一种基于PVS的PPTLI定理证明的形式化验证方法

作者：赵亮; 王祥坤; 段振华; 王小兵; 田聪; 张南

来源：2022-05-25, 中国, CN202210575903.7.

本发明涉及一种基于PVS的PPTLI定理证明的形式化验证方法,包括：S101：通过PVS构建得到PPTLI的基本时序类型和PPTLI的索引表达式类型,并根据PPTLI的索引表达式类型等价表示线性时序逻辑；S102：根据PPTLI的基本时序类型和PPTLI的索引表达式类型,通过PVS构建得到PPTLI定理证明系统；S103：将待证明的PPTLI时序性质表示为定理,利用PVS交互式证明命令使用PPTLI定理证明系统对待证明的PPTLI时序性质进行证明。本发明的方法借助于PPTLI这种表达能力强且综合统一的时序逻辑来描述和证明计算机系统预期的性质,能够弥补现有定理证明技术的不足,以保障系统的安全性和可靠性。

• 单位
  西安电子科技大学