買專利賣專利找龍圖騰，真高效！ 查專利查商標用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或微信搜索“龍圖騰網”。