基於路徑之驗證技術:理論與應用

Abstract

由於並行系統所具有的並行性、通訊與不可決定性等特質，並行系統通常相當複雜，而且難以分析其行為以確保其正確性。在眾多分析方法中，正規驗證被公認是一種相當有效方法。雖然目前有許多的方法可用以驗證並行系統，但是狀態爆炸的問題始終使得這些方法無法成功地完整驗證真正複雜的系統。該問題是指並性系統中的狀態隨著系統的大小成指數性的增長。針對此一問題，如果能夠將一複雜之系統分解成若干個較小的單元使得每個單元都能夠單獨被驗證，如此驗證的複雜度也會因被驗證的單元的大小降低，而有指數性的減低。根據此一想法，我們提出了基於路徑的驗證方法，該方法是將並行系統分解成一組由稱為並行路徑的個別執行行為所形成的集合。並行路徑是一種偏序的行為表示方法，此一方法分別記錄並行系統中各模組的相對應執行路徑。由於並行路徑可經由所有模組的路徑的卡氏積自動產生，而且可以被獨立驗證，對記憶體的需求取決於個別並行路徑的程度而非整個系統的大小。因此狀態爆炸的問題得以藉由此一「分割並逐一擊破」的方法而減輕，此外每個並行路徑的驗證都是獨立的因此可以很容易的並行處理來加快驗證的速度。 在本論文中，我們提出針對並行系統之基於路徑的驗證技巧與基於路徑的模型檢查技術。前者可用於檢查重要的邏輯性質，如死結與活結等。後者則可用於檢查由使用者以時序邏輯CTL所指定的的性質。這兩種方法可以較低的記憶體驗證任何可達性分析與CTL模型檢查所能驗證的性質。此外，我們也提出若干演算法，透過增加記憶體的使用量來加速驗證的效率，以及利用對稱驗證與平行驗證的技術來加速。我們利用兩個實際的系統X.21與Gigamax通訊協定來展示所提出方法的有效性。在這兩個例子中，與傳統的可達性分析與模型檢查方法相較，我們的方法都能夠有效的使用較少的記憶體進行驗證，並且在使用平行驗證的技術下，以較短的時間完成驗證的工作。

It is a challenging task to analyze the execution behavior and ensure the correctness of concurrent systems because their complexity introduced by the inherent nature of concurrency, communication and nondeterminism. Formal verification has been convinced to be an effective technique for such task. Many approaches have been proposed to verify concurrent systems, but the state explosion problem is the principal obstacle toward successful and complete verifications of complex systems. This problem refers to the phenomenon that the number of states in a concurrent system grows exponentially with the size of the system. One effective approach to alleviating the problem is to decompose the system into smaller units such that each one can be verified independently. The complexity of verifying smaller units is thus much smaller than that of the entire system. Based on this idea, we propose a new approach, called path-based verification approach. This approach is to decompose a concurrent system into a set of individual execution behaviors, denoted as concurrent paths. The concurrent path is partial-order representation recording the corresponding execution paths of individual modules of a concurrent system. The verification of individual concurrent paths then replaces that of the system. Since concurrent paths can be automatically generated through Cartesian product of the execution paths of all modules and they can be verified independently, the memory requirement is limited to the length of individual concurrent paths rather than the size of the entire system. The state explosion problem is hereafter alleviated from such "divide and conquer" approach. Furthermore, the verification can be performed in parallel since the analysis and verification of each concurrent path is independent. In this thesis, we propose path-based verification and path-based model checking techniques for concurrent systems based on the aforementioned idea. The former can verify the most critical properties, such as deadlock and livelock; the latter can the customized properties specified by the temporal logic CTL. Both methods can verify any properties that can be verified by reachability analysis or CTL model checking with less memory requirement. We also propose several algorithms, making trade-off on memory requirement to generate and analyze concurrent paths more efficiently, and utilizing the techniques of symmetric verification and parallel verification to improve efficiency. We also demonstrate the usefulness of our approach to the real systems, X.21 and Gigamax protocols. Both cases show that our approach uses less memory and takes less time if parallel verification technique is utilized than the original reachability analysis and model checking algorithms.