本發明公開了一種基于抽象模型的有限狀態機分析方法和系統，所述分析方法包括：使用編譯技術，將根據用戶描述構建的有限狀態機模型轉換為系統可識別的表示形式；使用編譯技術，從該表示形式的調用關系圖上自底向上訪問所有軟件單元，在單一軟件單元內部識別有限狀態機模型相關的轉換語句，并建立單一轉換語句的后繼訪問列表；遍歷所有的軟件單元，當識別出有限狀態機模型的初始轉換語句后，根據該轉換語句的后繼訪問列表，在軟件內部按照有限狀態機轉換語句的先后關聯關系遍歷軟件單元，并依據有限狀態機狀態轉換識別錯誤并報錯。在本發明中，可以覆蓋有限狀態機模型所關注問題的所有情形，實現針對所關注問題的無漏報、無錯報。

技術領域

本發明屬于狀態機技術領域，更具體地，涉及一種基于抽象模型的有限狀態機分析方法和系統。

背景技術

有限狀態機是一種表示有限個狀態以及在這些狀態之間的轉移和動作等行為的數學計算模型。在程序分析中，一些較為復雜的檢測規則也可以抽象為有限狀態機模型，指導分析算法的實現。然而，隨著程序規模的增長，程序內部邏輯愈發復雜，各種分支情況使得程序分析需要遍歷的路徑呈現指數級增長，通過全程序遍歷追蹤有限狀態機的狀態轉換捕抓錯誤愈發受限于資源消耗。同時，當前的程序分析工具和相關研究都只使用有限狀態機識別錯誤，實現中并沒有包含所關注問題在有限狀態機抽象模型上的正確流程，從而無法判斷所抽象的有限狀態機模型是否完整的覆蓋了所關注問題的所有情形，也就無法判斷該有限狀態機是否覆蓋了所關注問題的所有錯誤情形，難以實現針對所關注問題的無漏報、無錯報。

鑒于此，克服該現有技術產品所存在的不足是本技術領域亟待解決的問題。

發明內容

針對現有技術的以上缺陷或改進需求，本發明提供了一種基于抽象模型的有限狀態機分析方法和系統，其目的在于，通過該分析方法覆蓋有限狀態機模型所關注問題的所有情形，實現針對所關注問題的無漏報、無錯報。

為實現上述目的，按照本發明的一個方面，提供了一種基于抽象模型的有限狀態機分析方法，所述分析方法包括：

S1：使用編譯技術，將根據用戶描述構建的有限狀態機模型轉換為系統可識別的表示形式，其中，該表現形式包括多個軟件單元；

S2：使用編譯技術，從該表示形式的調用關系圖上自底向上訪問所有軟件單元，在單一軟件單元內部識別有限狀態機模型相關的轉換語句，并建立單一轉換語句的后繼訪問列表；

S3：遍歷所有的軟件單元，當識別出有限狀態機模型的初始轉換語句后，根據該轉換語句的后繼訪問列表，在軟件內部按照有限狀態機轉換語句的先后關聯關系遍歷軟件單元，并依據有限狀態機狀態轉換識別錯誤并報錯。

優選地，所述S2具體包括：

S21：判斷當前軟件單元是否還存在未訪問的語句；

S22：若存在未訪問的語句，則判斷當前語句是否為有限狀態機模型的狀態轉換關聯語句；

S23：若當前語句是有限狀態機模型的狀態轉換關聯語句，則標記當前語句為有限狀態機模型的狀態轉換關聯語句，將該語句加入到前一條轉換語句的后繼訪問列表，并將當前語句設置為前一條轉換語句。

優選地，所述S2還包括：

S24：若當前語句不是有限狀態機模型的狀態轉換關聯語句，則判斷當前語句是否為函數調用語句；

S25：若是函數調用語句，則判斷被調用函數是否包含有限狀態機模型的轉換語句；

S26：若包含有限狀態機模型的轉換語句，則標記當前語句為有限狀態機模型的函數調用關聯語句，將該語句加入到前一條轉換語句的后繼訪問列表，并將當前語句設置為前一條轉換語句。

優選地，所述S3包括：

S31：判斷當前軟件單元是否包含有限狀態機模型的初始轉換語句；