多執行緒Ｃ語言程式的顯式和符號模型驗證方法比較研究

Abstract

有兩種主要的方法來實現模型檢查過程，即顯式模型驗證和符號模型驗證。顯式模型驗證首先使用某種深度搜索算法為核心，同時結合偏序歸約技術限制探索狀態的數量。符號模型檢查基於布林函數的操作，代表狀態和路徑的集合，而不是顯式狀態路徑圖的遍歷。二元決策圖通常被使用於符號模型驗證器的實現。這兩種方法都有自己的優點和缺點。 本論文的目的是提供顯式模型驗證和符號模型驗證之間的比較並分析其比較結果。對於顯式模型驗證，我們採用在程序分析框架 Ultimate 中，基於巢狀深度優先搜索的一個模型驗證工具。對於符號模型驗證，我們實現了一個固定點模型驗證工具，它也是在 Ultimate 中被實作，並且使用 JavaBDD 套件作為二元決策圖輔助。我們使用可擴展的源代碼分析器 Scantu 來進行比較實驗。它允許通過其用戶界面選擇不同的模型驗證工具，因此我們可以在其中使用兩種方法來驗證各種 C 程式語言並進行比較。我們通過使用正確和錯誤的 C 程序和線性時序邏輯性質來設計不同的實驗，以產生更多樣化的比較結果。從實驗中，我們得出結論：在固定點計算期間，可達狀態和遍歷路徑的數量對於我們的模型驗證工具花費的時間有巨大影響。在這篇論文中，我們呈現比較結果並分析其原因。

There are two primary approaches to implementing the process of model checking, namely explicit-state model checking and symbolic model check ing. Explicit-state model checking uses some depth first search algorithm as the core, while incorporating partial-order reduction techniques to limit the number of states explored. Symbolic model checking is based on the manip ulation of Boolean functions, which represent sets of states and transitions, rather than the traversal of explicit-state transition graphs. Binary decision diagrams are often used to support the implementation of a symbolic model checker. Both approaches have their own strengths and weaknesses. The aim of this thesis is to provide a comparison between explicit model checking and symbolic model checking and to analyze the results of the com parison. For the explicit approach, we adopt an existing implementation of nested depth first search based on the Ultimate program analysis frame work. For the symbolic approach, we implement a fixpoint model checker, also based on Ultimate and using JavaBDD as our BDD package. We use Scantu, an extensible source code analyzer, to facilitate the comparison. It allows the choice of different model checkers through its user interface, so we can alternate between the two approaches to verify various target C programs and carry out the comparison easily. We design different experimental set tings by using different correctness combinations of temporal properties and C programs to produce more diverse comparison results. From the experi ments, we conclude that the number of reachable states has a huge impact on the time spent, and so does the number of traversed transitions during the fixpoint calculation. We present the comparison results and analyze their causes in this thesis.