买专利卖专利找龙图腾，真高效！ 查专利查商标用IPTOP,全免费！专利年费监控用IP管家,真方便！

龙图腾网恭喜西安电子科技大学申请的专利一种基于PVS的PPTLI定理证明的形式化验证方法获国家发明授权专利权，本发明授权专利权由国家知识产权局授予，授权公告号为：CN115080112B 。

龙图腾网通过国家知识产权局官网在2025-05-13发布的发明授权授权公告中获悉：该发明授权的专利申请号/专利号为：202210575903.7，技术领域涉及：G06F8/75；该发明授权一种基于PVS的PPTLI定理证明的形式化验证方法是由赵亮;王祥坤;段振华;王小兵;田聪;张南设计研发完成，并于2022-05-25向国家知识产权局提交的专利申请。

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

本发明授权一种基于PVS的PPTLI定理证明的形式化验证方法在权利要求书中公布了：1.一种基于PVS的PPTLI定理证明的形式化验证方法，其特征在于，包括：S101：通过PVS构建得到PPTLI的基本时序类型和PPTLI的索引表达式类型，并根据所述PPTLI的索引表达式类型等价表示线性时序逻辑；S102：根据所述PPTLI的基本时序类型和所述PPTLI的索引表达式类型，通过PVS构建得到PPTLI定理证明系统；S103：将待证明的PPTLI时序性质表示为定理，利用PVS交互式证明命令使用所述PPTLI定理证明系统对所述待证明的PPTLI时序性质进行证明；所述PPTLI的索引表达式具有如下形式： 式中，表示无穷或操作，R表示索引项包括○iP、Pi和Pi三种基本索引项，其中，○iP表示对P应用i次○操作，Pi表示P重复成立i次，Pi表示P从当前状态开始连续成立i个状态；通过PVS构建得到PPTLI的索引表达式类型，包括：步骤a：根据所述PPTLI的索引表达式将所述索引项定义为函数IE：[nat-PPTLI]，将所述无穷或操作定义为函数OrInf:[IE-PPTLI]，并得到所述索引表达式在PVS中的形式化描述OrInfR，其中，R表示IE类型的变量；步骤b：在PVS中通过RECURSIVE关键字将基本索引项○iP定义为函数类型NextIP，基本索引项Pi定义为函数类型ChopIP，基本索引项Pi定义为函数类型ConsIP；步骤c：通过PVS定义索引项连接词，其中，所述索引项连接词包括表示索引项之间的非、合取、下一状态、顺序复合加和投影的连接操作，将所述索引项之间的非、合取、下一状态、顺序复合加和投影的连接操作分别定义为函数类型INot、IAnd、INext、IPlus和IPrj；步骤d：通过PVS构造特殊索引项类型，所述特殊索引项类型表示不含索引的PPTLI类型与索引项类型之间的等价转换，将不含索引的PPTLI类型与索引项类型之间的等价转换定义为函数类型toIEP。

如需购买、转让、实施、许可或投资类似专利技术，可联系本专利的申请人或专利权人西安电子科技大学，其通讯地址为：710071 陕西省西安市太白南路2号；或者联系龙图腾网官方客服，联系龙图腾网可拨打电话0551-65771310或微信搜索“龙图腾网”。