符號執行和模型檢查

符號執行和模型檢查（例如在模型轉換中）有什麼區別？我不明白他們的區別。他們是一樣的嗎？！符號執行和模型檢查

來源

2016-08-23 any

在模型檢查中，您必須將您的系統編碼爲有限狀態機，並將該FSM提供給模型檢查器以及規範。模型檢查器將確保規範始終在該系統中。

在符號執行中，您只提供程序，符號執行引擎將檢查所有可行路徑以生成測試輸入或檢查斷言。

一個簡單的例子：併發性。模型檢查可以處理多線程系統，因爲它在作爲輸入提供的FSM中指定，但符號執行不能處理多個線程。

來源

2016-09-06 20:43:40 afsafzal

感謝你的幫助。 Java Path Finder是模型檢查工具還是符號執行工具或兩者？是否有任何不使用模型檢查的符號執行工具？ – any

模型檢查：正式驗證程序是否滿足規範的方法。規範通常以一個時態邏輯公式給出，如：「如果輸入是x輸出必須是y - 對於程序的所有執行（全局）」（例如參見Edward A Lee）。

符號模型檢查與顯式狀態檢查：程序可以是有限狀態機（FSM）。這裏明確的狀態檢查就足夠了。但幸運的是，模型檢查器也適用於擴展的FSM，併發，概率，實時應用程序。爲了幫助防止具有非常大（無限）狀態的系統中的狀態爆炸，使用符號模型檢查。在符號模型中檢查狀態和輸入等被視爲符號和命題公式（或狀態集合，集合操作等）。爲了執行模型檢查，需要進行可達性分析，並執行此操作，程序轉換將以符號方式執行。這些檢查程序不能使用工具化本機代碼的正常執行。

符號執行：在符號執行過程中存在不同的編碼方法。有些模型檢查非常具體，有些模塊是模塊化的，並且在象徵執行的發明人所定義的獨立符號執行框架中使用。一個象徵性的執行框架也經常使用符號模型檢驗的某些元素（勘探，搜索），以用於測試等是可用的

最後一些例子：

JPF，Java的探路者：模型檢查，明確檢查狀態，輸入：Java字節碼

SPF，符號探路者：符號執行，JPF

JCBMC的延伸：界的模型檢查器，JPF的擴展，SPF

XRTs：探索與符號IC執行，輸入：CIL字節碼

IntelliTest：參數化單元測試使用XRTs

規格資源管理器：基於模型的測試使用XRTs

來源

2017-04-15 13:33:51 goofy

符號執行和模型檢查

回答

相關問題