[發明專利]一種面向計算平臺的系統評估裝置

在審

• 申請號: 202110785853.0
• 申請日: 2021-07-12
• 公開（公告）號: CN113553246A
• 公開（公告）日: 2021-10-26
• 發明（設計）人: 黃滟鴻;肖思慧;史建琦;郭欣;楊洋
• 申請（專利權）人: 華東師范大學
• 主分類號: G06F11/34
• 分類號: G06F11/34;G06F11/36
• 代理公司: 北京辰權知識產權代理有限公司 11619
• 代理人: 付婧

1.一種面向計算平臺的系統評估裝置，其特征在于，包括以下步驟：

公式轉換模塊：用于根據計算機的非形式化描述語言轉化得到符號邏輯的等價公式；

霍爾三元組模型模塊：用于根據所述符號邏輯的等價公式構建得到霍爾三元組模型；

部分正確性驗證模塊：用于根據所述霍爾三元組模型進行自動路徑測試，得到模型部分正確性結果；

完全正確性驗證模塊：用于根據所述霍爾三元組模型分析系統程序終止性，得到模型完全正確性結果。

2.根據權利要求1所述的面向計算平臺的系統評估裝置，其特征在于，所述公式轉換模塊的非形式化描述語言通過采用一階邏輯對非形式化的計算機語言進行描述得到。

3.根據權利要求1所述的面向計算平臺的系統評估裝置，其特征在于，所述霍爾三元組模型模塊，具體包括：

霍爾邏輯單元：用于基于霍爾邏輯對所述符號邏輯的等價公式進行建模，構造得到形式化的霍爾三元組模型。

4.根據權利要求1所述的面向計算平臺的系統評估裝置，其特征在于，所述部分正確性驗證模塊，具體包括：

符號執行單元：用于通過符號執行方法對所述霍爾三元組模型進行自動路徑測試。

5.根據權利要求1所述的面向計算平臺的系統評估裝置，其特征在于，所述部分正確性驗證模塊，具體包括：

數理邏輯斷言單元：用于確定所述霍爾三元組模型的描述程序部分正確性的的數理邏輯斷言{P}C{Q}；

執行單元：用于從滿足所述數理邏輯斷言{P}C{Q}的斷言P的狀態開始，以符號執行的方式開始執行直至執行中止；

部分正確性評估單元：用于若中止時狀態滿足所述數理邏輯斷言{P}C{Q}的斷言Q，則評估霍爾三元組模型滿足部分正確性；用于若中止時狀態不滿足所述數理邏輯斷言{P}C{Q}的斷言Q，則評估霍爾三元組模型不滿足部分正確性。

6.根據權利要求5所述的面向計算平臺的系統評估裝置，其特征在于，所述霍爾三元組模型不滿足部分正確性時，還包括輸出不滿足部分正確性原因。

7.根據權利要求1所述的面向計算平臺的系統評估裝置，其特征在于，所述完全正確性驗證模塊，具體包括：

啟發式搜索單元；用于采用啟發式搜索算法搜索霍爾三元組模型路徑。

8.根據權利要求7所述的面向計算平臺的系統評估裝置，其特征在于，所述啟發式搜索單元包括深度優先搜索算法或廣度優先搜索算法。

9.根據權利要求1所述的面向計算平臺的系統評估裝置，其特征在于，所述完全正確性驗證模塊，具體包括：

冗余路徑剪枝單元：用于采用冗余路徑剪枝方法對確定的冗余路徑進行剪枝。

10.根據權利要求1所述的面向計算平臺的系統評估裝置，其特征在于，所述完全正確性驗證模塊得到模型完全正確性結果為霍爾三元組模型不滿足完全正確性時，還包括輸出不滿足完全正確性原因。