[發明專利]一種基于插值的模型檢測路徑縮減方法、計算機

有效

• 申請號: 201710896756.2
• 申請日: 2017-09-28
• 公開（公告）號: CN107844415B
• 公開（公告）日: 2021-02-05
• 發明（設計）人: 田聰;段釗;段振華
• 申請（專利權）人: 西安電子科技大學
• 主分類號: G06F11/36
• 分類號: G06F11/36
• 代理公司: 西安長和專利代理有限公司 61227
• 代理人: 黃偉洪;何畏

1.一種基于插值的模型檢測路徑縮減方法，其特征在于，所述基于插值的模型檢測路徑縮減方法讀入C程序，對C程序進行語法語義分析，并從抽象語法樹中提取出控制流圖CFG；給CFG添加safety插值和error插值，擴展CFG；在根據CFG生成抽象可達圖ARG的過程中，在每一個狀態，判斷safety插值和error插值是否被當前路徑公式蘊含；

如果某一個狀態的error插值被蘊含，則說明程序存在一條真反例路徑，程序不安全，驗證結束；如果safety插值被蘊含，則說明該狀態的后續所有路徑都是安全的，不需要遍歷，減少了遍歷的路徑；如果發現一個虛假反例路徑，則根據Craig插值，計算和更新safety插值和error插值；

所述基于插值的模型檢測路徑縮減方法包括以下步驟：

步驟一，根據待驗證的程序，生成控制流圖CFG，給CFG中的結點添加3個屬性:R插值，S插值和E插值，R插值是結點可達的約束條件，判斷一個狀態的可達性；S插值和E插值對路徑進行規約，加快程序的驗證；給CFG的邊添加屬性W；一條邊的W值表示以該邊指向的結點為根結點的子圖中，還沒有被遍歷的分支的個數；

步驟二，根據生成的CFG，生成抽象可達圖ARG，如果沿著一條路徑生成一個新狀態s，如果s對應的R插值被滿足，說明狀態s可達，繼續沿著狀態s遍歷該路徑；否則，狀態s不可達，則該路徑終止，遍歷其他路徑；對于一個可達的狀態s，如果狀態s對應的E插值被該路徑對應的路徑公式蘊含，說明沿著該狀態存在一條到達目標狀態的路徑，程序不安全；如果狀態s對應的S插值被蘊含，說明以狀態為起點的所有路徑都是安全的，不需要沿著狀態s探索程序；如果狀態s是可達的，且E插值和S插值都不被蘊含，則繼續沿著狀態s遍歷該路徑；

步驟三，在生成ARG的過程中，發現一條反例路徑，到達目標狀態，則需要進一步判斷反例路徑是否虛假；不是虛假反例，則說明程序是不安全的；否則，根據虛假反例，細化模型，分別計算并更新對應狀態的R插值，S插值和E插值，執行重新生成ARG，直到找到一條真反例路徑或不存在反例路徑。

2.如權利要求1所述的基于插值的模型檢測路徑縮減方法，其特征在于，所述步驟一根據待驗證的程序，生成控制流圖CFG，并且初始化結點和邊的屬性，包括以下步驟：

(1)找到CFG中的目標結點，從目標結點開始反向遍歷CFG，遍歷的結點和邊都保留，沒有遍歷到的結點和邊都刪除；

(2)得到裁剪后的CFG，初始化屬性的值，對各個結點的三種插值進行初始化，初次遍歷CFG，生成ARG的過程中，每一個結點的R插值的初始值都為{true}；對于S插值，定義了為一個二元組:(F,I_s)，其中，F的值域為{full,half}，I_s的值是一個由謂詞組成的合取式；對于一個結點l，如果l沒有后繼結點或者l的所有后繼結點的S插值都是full,記為f，表示l的所有后繼結點都被遍歷過，則l的S插值也是full，否則，l的S插值為half，記為h，具體的形式如下：

若l是終結點，S插值的初始值為(full,true)，表示如果到達終結點，路徑一定是安全的；若l是目標結點，S插值的初始值為(full,false)，表示如果到達目標結點，路徑一定是反例路徑；對于其他結點，S插值的初始值為(half,true)，具體的形式如下:

若l是目標結點，E插值的初始值為true，表示路徑一定是真反例；若l是終結點，E插值的初始值為false，表示路徑一定不可能到達目標結點；對于其他結點，E插值的初始值為false，初始認為都不能到達目標結點；對于每一條遷移的W屬性，初始值為⊥，表示還沒開始遍歷，其中，W的值域為{N+,⊥}，N+是正整數集合。