[發(fā)明專利]基于SAT的命題投影時序邏輯限界模型檢測方法

有效

• 申請?zhí)枺?/td>: 201210102064.3
• 申請日: 2012-04-09
• 公開（公告）號: CN102663191A
• 公開（公告）日: 2012-09-12
• 發(fā)明（設計）人: 段振華;何佳;田聰;王小兵
• 申請（專利權）人: 西安電子科技大學
• 主分類號: G06F17/50
• 分類號: G06F17/50
• 代理公司: 陜西電子工業(yè)專利中心 61205
• 代理人: 程曉霞;王品華

1.一種基于SAT的命題投影時序邏輯限界模型檢測方法，其特征在于：具體檢測步驟包括：

步驟1.首先為待驗證系統(tǒng)建立模型M，M是一個描述待驗證系統(tǒng)行為的有限狀態(tài)遷移系統(tǒng)，采用Kripke結構描述模型M；

步驟2.使用命題投影時序邏輯PPTL公式描述待驗證系統(tǒng)的性質，得到PPTL描述的性質公式P，并將其等價轉換為正則形NF，得到性質公式P的正則形NF(P)，進而得到性質非的正則形

步驟3.設定限界模型檢測的界限k，k為一個不大于完整區(qū)間長度的正整數(shù)，用來限定進行限界模型檢測時的搜索長度，界限k的值在一個限界模型檢測周期內(nèi)是不變的，在下一個限界模型檢測周期內(nèi)可根據(jù)當前周期的檢測結果進行調整；

步驟4.根據(jù)PPTL限界模型檢測向命題可滿足性問題SAT轉換的轉換規(guī)則，結合設定的限界模型檢測界限k，對待驗證系統(tǒng)模型M和性質的非進行編碼，通過布爾編碼將限界模型檢測問題轉化為命題可滿足性SAT問題；

步驟5.使用SAT求解器對SAT問題進行求解：有解，說明待驗證系統(tǒng)M不滿足性質P，給出相應的反例；無解，說明待驗證系統(tǒng)M?k-有界滿足性質P，再增大界限k的值，跳至步驟3，進入下一個限界模型檢測周期，直到k的值足夠大并且在每個限界模型檢測周期內(nèi)待驗證系統(tǒng)M都是k-有界滿足性質P的，認為待驗證系統(tǒng)M滿足性質P，結束限界模型檢測過程。

2.根據(jù)權利要求1所述的基于SAT的命題投影時序邏輯的限界模型檢測方法，其特征在于：將PPTL限界模型檢測問題轉換為命題的可滿足性問題的具體步驟包括：

步驟4.1.根據(jù)待驗證系統(tǒng)Kripke結構模型M的標記函數(shù)L，用布爾向量表示待驗證系統(tǒng)中的狀態(tài)和遷移關系，完成待驗證系統(tǒng)約束條件的編碼過程，約束條件其中k為界限，I(s₀)表示狀態(tài)s₀是初始狀態(tài)，T(s_i，s_i+1)表示從狀態(tài)s_i到狀態(tài)s_i+1的狀態(tài)遷移關系，表示狀態(tài)序列(s₀，s₁，...，s_k)中從狀態(tài)s₀經(jīng)過狀態(tài)s₁，s₂，...，s_i，...，s_k-1到達狀態(tài)s_k的一系列狀態(tài)遷移，若狀態(tài)序列(s₀，s₁，...，s_k)是從初始狀態(tài)出發(fā)的有效區(qū)間，則存在一組賦值使得約束條件M_k為真；

步驟4.2.在界限k下，將待驗證系統(tǒng)性質P轉換為等價的命題公式：待驗證系統(tǒng)的性質P的約束條件L_k是在界限k下區(qū)間的循環(huán)條件，根據(jù)搜索區(qū)間的結構，確定區(qū)間結構相關部分L_k的真假值，區(qū)間為有循環(huán)的無窮區(qū)間時，L_k為真，區(qū)間為無循環(huán)的有窮區(qū)間時，L_k為假；根據(jù)限界模型檢測過程中PPTL性質公式P向命題公式的等價轉換規(guī)則，對性質約束條件中性質相關部分和進行等價轉換，進而得到約束條件X_k等價的命題公式，其中0為初始狀態(tài)s₀下標，k為界限，l為狀態(tài)s_l下標，是無循環(huán)有窮區(qū)間下的性質約束條件，記錄了所有可能的從狀態(tài)s_k到之前狀態(tài)的遷移，L_(k，l)表示存在從狀態(tài)s_k到向前狀態(tài)s_l(l∈N，0≤l≤k)的狀態(tài)遷移，循環(huán)的狀態(tài)序列段為(s₁，...，s_k)，表示在界限k內(nèi)，該區(qū)間是無循環(huán)有窮的區(qū)間，是無循環(huán)有窮區(qū)間在界限k下的性質相關部分；是有循環(huán)無窮區(qū)間下的性質約束條件，是有循環(huán)無窮區(qū)間在界限k下的性質相關部分，表示所有可能的循環(huán)及其相應的性質約束；

步驟4.3.將步驟4.1和步驟4.2得到的約束條件M_k和X_k的等價命題公式合并，得到PPTL限界模型檢測問題的形式化描述：及其等價命題公式F，完成限界模型檢測問題向SAT問題的轉換。