[發明專利]一種針對軟件模型檢查工具的測試用例自動生成方法和系統

在審

• 申請號: 202110575863.1
• 申請日: 2021-05-26
• 公開（公告）號: CN113434385A
• 公開（公告）日: 2021-09-24
• 發明（設計）人: 嚴懿宸;張棖宇;蘇亭;蒲戈光
• 申請（專利權）人: 華東師范大學
• 主分類號: G06F11/36
• 分類號: G06F11/36
• 代理公司: 上海德禾翰通律師事務所 31319
• 代理人: 夏思秋

1.一種針對軟件模型檢查工具的測試用例自動生成方法，其特征在于，所述方法包括如下步驟：

步驟一、使用Clang編譯器前端對待測試的源代碼進行分析，根據分析結果插入用于記錄程序運行狀況的樁語句，不改變程序原本的邏輯；

步驟二、編譯并運行步驟一中插入樁語句后的程序，獲得程序運行過程中的狀態；

步驟三、對源程序進行處理，將程序實際的運行狀態作為待檢查的條件判斷，嵌入源代碼產生測試用例，使軟件模型檢查工具能夠判斷自身結果是否與實際運行結果一致；

步驟四、以步驟三得到的測試用例運行軟件模型檢查工具，得到檢查工具在該測試用例上正確與否的結果。

2.如權利要求1所述的方法，其特征在于，所述軟件模型檢查工具為針對C語言的軟件模型檢查工具，包括CBMC、CPAChecker、SeaHorn。

3.如權利要求1所述的方法，其特征在于，所述步驟一進一步包括以下子步驟：

步驟1.1、基于控制流分析的技術和Clang編譯器前端對源代碼進行分析，得到包括源代碼中各個分支、循環的位置和數量信息的分析結果；

步驟1.2、根據所述分析結果，在源代碼對應位置插入樁語句；

其中，所述Clang編譯器前端為Clang編譯器的前端解析工具，用于實現針對C程序的分析算法及工具；

所述待測試的源代碼來源于可編譯及運行的通用C源代碼；

所述樁語句及其插入位置為：1)對于源代碼中的每一個循環，在程序開頭插入1整形變量，用于記錄循環運行的次數，在循環內根據不同的策略更新變量的值；2)對于源代碼中的每一個分支判斷，在程序開頭插入2整形變量，用于記錄各分支運行的次數，根據不同的策略更新變量的值；3)對于源代碼中的每一個退出點，插入打印語句，使程序在退出前輸出所述插入的記錄變量。

4.如權利要求1所述的方法，其特征在于，所述步驟二進一步包括以下子步驟：

步驟2.1、編譯步驟一處理過后的源代碼，得到可執行文件；

步驟2.2、運行獲得的可執行文件，獲得所述步驟一中插入的每個記錄變量的值；

其中，所述編譯運行中使用的編譯器為GCC編譯器；

所述記錄變量的值包括通過所述步驟一所插入樁語句獲得的源代碼中每個循環、分支判斷的運行次數。

5.如權利要求1所述的方法，其特征在于，步驟三中，所述對源程序的處理為根據所述步驟二中獲得的狀態，插入ASSERT語句，用于構建符合程序實際執行狀態的，可用于軟件模型檢查工具的測試用例；

其中，所述ASSERT語句為源代碼中軟件模型檢查工具需要檢查的條件；

所述所插入ASSERT語句的判斷條件在程序實際執行狀態范圍內，因此實現正確的軟件模型檢查工具應始終返回“可滿足”的結果。

6.如權利要求5所述的方法，其特征在于，所述ASSERT語句的插入通過三種策略，包括：分支可達性策略、分支計數策略、分支計數范圍策略；

所述分支可達性策略是指對于程序中每一個分支判斷，在程序開始創建2整型變量，用于記錄各分支判斷是否被執行；在各分支內將對應的變量設為1；在程序退出點插入ASSERT語句，檢查的表達式為根據程序實際執行結果得到的各分支執行與否信息構建的條件語句；

所述分支計數策略是指對于程序中每一個分支判斷，在程序開始創建2整型變量，用于記錄各分支判斷被執行的次數；在各分支內將對應的變量增加1；在程序退出點插入ASSERT語句，檢查的表達式為根據程序實際執行結果得到的各分支執行次數信息構建的條件語句；

所述分支計數范圍策略是指對于程序中每一個分支判斷，在程序開始創建2整型變量，用于記錄各分支判斷被執行的次數；在各分支內將對應的變量增加1；在各分支內插入ASSERT語句，檢查的表達式為當前分支執行次數是否在程序實際執行次數范圍內。