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

有效

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

本發明屬于計算機應用技術領域，公開了一種基于插值的模型檢測路徑縮減方法、計算機，讀入C程序，對C程序進行語法語義分析，并從抽象語法樹中提取出控制流自動機CFG；給CFG添加safety(S)插值和error(E)插值，擴展CFG；在根據CFG生成ARG的過程中，在每一個狀態，判斷safety插值和error插值是否被當前路徑公式蘊含。本發明通過計算S插值和E插值，提高了檢測的效率，使得模型檢測算法可以更好地應用于大規模的程序；S插值避免不必要的探索，大大地減少ARG的狀態數；E插值可以運用于快速地判斷程序中是否存在真反例路徑，加快了程序的驗證，提高了效率；裁剪CFG中無用結點和邊，縮小了遍歷狀態空間。

技術領域

本發明屬于計算機應用技術領域，尤其涉及一種基于插值的模型檢測路徑縮減方法、計算機。

背景技術

隨著科技的快速發展和工業需求的不斷提高，各種軟硬件設計的的復雜度也日益增加，對于可靠性和安全性的要求也不斷提高。系統的可靠性，安全性和正確性已經受到了科學界和工業界的廣泛關注。形式化驗證和測試是解決該問題的主要方法。形式化驗證方法始于20世紀60年代末的Floyd、Hoare和Manna等在程序規范和驗證方面的研究。形式化驗證方法分為兩大類：基于定理證明和基于模型。20世紀80年代初提出的模型檢測(ModelChecking)屬于基于模型的形式化驗證方法，思想相對簡單和自動化程度高，可以廣泛用于硬件電路系統和網絡協議系統的驗證。模型檢測就是先把系統建模為有限狀態轉移系統，并用時態邏輯描述特驗證的規范，在有限狀態轉移系統上進行窮盡搜索，確定規范是否被滿足，若沒有滿足，給出反例指出為什么沒有滿足。模型檢測面臨狀態爆炸問題，所謂狀態爆炸問題即系統狀態數隨著狀態規模的增加呈指數級增加。所以該領域的研究人員使用各種方法縮減搜索的狀態空間，基于反例引導的抽象模型檢測是常用的技術。基于反例路徑的抽象細化(Counterexample-Guided Abstraction Refinement，CEGAR)技術的過程如下：給定一個模型和性質，首先通過抽象的方法生成一個抽象模型。抽象模型包含的行為可能會多于原始模型，但是，抽象模型的結構和描述都比原始模型簡單，所以可以緩解狀態空間爆炸問題。然后調用模型檢測器，檢測公式是否在抽象模型中有效。如果有效，則程序終止；否則，會給出反例路徑，然后進行重構(reconstruction)過程，即在原始模型中，如果成功找到一條路徑對應于反例路徑，則程序結束；否則，反例路徑為虛假反例路徑，下一個迭代過程開始，重新生成抽象模型，進行驗證。重復此過程，直到返回有效或者無效，或者狀態空間爆炸造成程序停止。動態符號執行技術是一種符號執行與具體執行相結合的測試手段。符號執行是指在不執行程序的前提下，用符號值表示程序變量的值，然后模擬程序執行來進行相關分析。首先，對待分析代碼構建控制流圖(Control Flow Graph，CFG)，它是編譯器內部用有向圖表示一個程序過程的抽象數據結構。在CFG上從入口節點開始模擬執行，在遇到分支節點時，使用約束求解器判定哪條分支可行，并根據預先設計的路徑調度策略實現對該過程所有路徑的遍歷分析，最后輸出每條可執行路徑的分析結果。動態符號執行是以具體數值作為輸入，同時啟動代碼模擬執行器，并從當前路徑的分支語句的謂詞中搜集所有符號約束。然后根據策略反轉約束中的一個分支，構造一條新的可行的路徑約束，并用約束求解器求解出一個可行的新的具體輸入，接著符號執行引擎對新輸入值進行新一輪的分析。通過使用這種輸入迭代產生新輸入的方法，理論上所有可行的路徑都可以被計算并分析一遍。動態符號執行技術的主要瓶頸是路徑爆炸問題，即隨著程序中分支數的增多，路徑呈指數級增加。插值是緩解路徑爆炸問題的有效方法，主要是一種搜索剪枝的思想，通過利用不可行路徑給行節點標記插值，插值是指一定不會到達被標記為錯誤行的條件約束。對于分支節點，若該節點的每個分支都被探索過，那么在該節點標記的插值為全插值，否則為半插值。在動態符號執行中，若從開始節點到當前節點的路徑約束滿足當前節點的全插值，則該路徑可被歸并，即不被探索，從而有效緩解了路徑爆炸問題。對于大規模系統，抽象模型在進行驗證時細化次數過多。細化的次數越多，占用的時間就越多。每次細化后，都要重新構建抽象模型，重復遍歷的許多路徑，降低了驗證效率。而且驗證模型時，產生的狀態數隨系統的規模和復雜性增大而增大，會引起狀態空間爆炸問題，從而消耗大量的內存和時間，導致驗證崩潰，因此，在驗證的過程中，找到一種方法，可以減少遍歷的路徑和細化的次數，快速地對程序進行驗證，從而降低狀態數，使之可以對大規模的程序進行驗證，已經成為一個亟待解決的問題。