基於自動機的多執行緒程式模型驗證工具支援

Abstract

基於自動機的時序邏輯模型驗證牽涉到兩個Büchi自動機，一個代表被驗證系統的行為，另一個描述違背時序規範的行為。如果系統違反給定的性質，則在由系統自動機和性質自動機所構成的同步乘積中存在一個套索狀的路徑。當系統中有平行運行的程序時，系統自動機由多個程序的自動機的不同步乘積構成，代表輸入的多執行緒程式的交錯執行，每個自動機代表一個執行緒。有鑑於包含全部交錯執行的全域狀態空間過分地龐大，必須運用偏序縮減，在保留正確性的同時生成精簡的狀態空間。 這篇論文旨在創立一個便利基於自動機的多執行緒程式模型驗證實作的函式庫。這個函式庫建立在Ultimate程式分析框架中，它包含一個主要的類別，可用來接受控制流程圖和由現有部件生成的性質自動機。此主要類別提供基礎的模型驗證方法，包括從控制流程圖即時生成系統狀態、特定狀態對外轉移的可行性檢查以及實際執行一個選定的轉移。其中也包含偏序縮減的一個重要步驟：基於安全度的程序重新排序方法。在Ultimate的模組化架構下，輸入的程式和規格被轉譯成中間語言Boogie，因此隨後的分析能脫離輸入語言特定語法的限制。我們的工具支援為多執行緒程式全域狀態空間的即時探索打下基礎，不同的基於自動機模型驗證演算法因此能被方便地實作出來。