多執行緒C語言程式的可擴展模型檢測工具

Abstract

模型檢測是一種用於驗證程式正確性的全自動方法，這對於軟體安全至關重要。最常用的方法之一是顯式狀態模型檢測。它可以使用各類深度優先搜索演算法來執行，被廣泛用於驗證可以用線性時序邏輯描述的屬性。若程式不正確，驗證期間將會回報違背被驗證屬性的程式執行行為。由於多執行緒程式在實務中非常普遍，因此可以驗證多執行緒程式屬性的模型檢測工具非常有價值。 在本論文中，我們構建了一個名為SCANTU的可擴展模型檢測工具，它具有用於驗證多執行緒C語言程式的可視化用戶界面。我們的工具建立在插件導向的ULTIMATE程式分析框架之上，該框架具有構建可擴展應用程式的良好架構。我們為用戶提供便利的方法來使用由ULTIMATE開發人員構建的插件擴展SCANTU。例如，擴展後，SCANTU用戶可以通過我們的用戶界面執行其他開發者設計的模型檢測演算法。這賦予了SCANTU工具箱的特性，允許用戶將自己需要的插件作為工具添加到SCANTU中，並根據情況選擇合適的工具。隨著ULTIMATE開發人員實作的模型檢測演算法越來越多，用戶可以使用我們的工具輕鬆比較不同演算法之間的執行效率。SCANTU還提供了基本的嵌套深度優先搜索(NDFS)演算法和幾種優化技術來提高效率。我們在論文中展示了我們工具的測試結果，包括多執行緒系統公平性的影響以及我們優化技術的性能。

Model checking is a fully automatic method for verifying the correctness of a program, which is essential for software safety. One of the most commonly used approaches is explicit-state model checking. It may be carried out using variants of depth-first search and is widely adopted to verify properties that can be described in linear temporal logic. An error trace if existing will be found during the verification. As multithreaded programs are very common in practice, model checking tools that can verify the properties of multithreaded programs are valuable. In this thesis, we build an extensible model checking tool called SCANTU with a visual user interface for multithreaded C programs. Our tool is built on the plugin-based ULTIMATE program analysis framework, which has a good architecture for building extensible applications. We provide convenient methods for users to extend SCANTU with plugins constructed by ULTIMATE developers. For example, after extension, SCANTU users can execute model checking algorithms designed by other developers through our user interface. This gives our tool characteristics of a toolbox, allowing users to add the plugins they need as tools to SCANTU, and select the appropriate tools according to the situation. As more model checking algorithms are implemented by ULTIMATE developers, users can easily compare the execution efficiencies between different algorithms with our tool. SCANTU also provides the basic nested depth-first search (NDFS) algorithm and several optimization techniques to improve its efficiency. We present in the thesis the test results of our tool, including the effect of fairness conditions and the performance of our optimization techniques.