基於自動機的模型檢查的深度優先搜尋演算法比較研究

Abstract

外顯式狀態模型檢查器以即時方式構建自動機以表示程式與否定屬性 的同步乘積，並使用深度優先搜尋探索自動機狀態。如果一個系統不滿足 某個性質，那麼自動機中有一條套索形狀的路徑，對應於系統的錯誤軌 跡。這種套索由一個句柄組成，該句柄顯示系統最初是如何演變的，然後 是一個循環，該循環表示系統可能無限期地遵循的重複行為。錯誤軌跡的 深度優先搜尋可以通過兩種不同的方式進行:巢狀深度優先搜尋和基於強 連通單元的搜尋。在一個巢狀深度優先搜尋中，第一個深度優先搜尋找到 可達的接受狀態，第二個深度優先搜尋從一個接受狀態進行搜尋，看該狀 態是否從自身可達，形成一個接受循環。另一方面，基於強連通單元的搜 尋包括找到可到達的強連通單元並檢查其中一個單元中是否存在接受狀 態，肯定的回答表明存在錯誤軌跡。 為了比較巢狀深度優先搜尋和基於強連通單元的演算法，我們將它們 實作為 Ultimate 程式分析框架的插件。該實作將動態模型檢查與偏序縮 減相結合，從而消除了驗證所檢查屬性所不需要的狀態。感謝 Ultimate 的支持，我們能夠將 C 語言中的多執行緒程式作為輸入，使這項工作變得 實用。該實作能夠重現存在於原始程式語句中的反例與相應的屬性狀態配 對，這有助於排除錯誤。我們使用選擇的基準案例來比較演算法的性能， 並在不同的場景下測試程式，例如不同的線性時間方程式、不同語句中的 錯誤以及執行緒的重複次數。除了提供對兩種深度優先搜索的見解外，這 項工作還可以構成模型檢查器的基礎，其中可以選擇不同的驗證方法以適 應不同的驗證任務。

Explicit-state model checkers build, in an on-the-fly fashion, an automaton representing the synchronous product of the program and the negated property and explore the automaton states using depth-first search. If a system does not satisfy a property, then there is a lasso-shaped path in the automaton that corresponds to an error trace of the system. Such lassos consist of a handle that shows how the system initially evolves, followed by a cycle that presents a repetitive behavior the system may follow indefinitely. The depth-first search of an error trace may be carried out in two different ways: nested depth-first search (NDFS) and strongly connected component (SCC)-based search. In an NDFS, the first DFS finds the accepting states that are reachable and the second DFS explores from an accepting state to see whether the state is reachable from itself to form an accepting cycle. On the other hand, an SCC-based search consists of finding the reachable SCCs and checking whether an accepting state exists in one of these components, an affirmative answer to which indicates the existence of an error trace. To compare NDFS and SCC-based algorithms, we implement them as plugins of the Ultimate program analysis framework. The implementation combines on-the-fly model checking with partial order reduction which eliminates the states that are not necessary for the verification of the checked property. Thanks to the support of Ultimate, we are able to take multithreaded programs in C as input, making this work practically useful. The implementation is capable of reproducing a counter-example that exists in the original program statements paired with the corresponding property states, which is helpful for debugging. We compare the performances of the algorithms using a selection of benchmark cases and testing the programs under different scenarios, such as different linear temporal formulae, errors in different statements, and repeating times of the threads. Besides providing insights into the two types of depth-first search, this work may also form the basis of a model checker where different verification methods may be selected to suit different verification tasks.