[發明專利]一種面向計算平臺的自動評估方法

在審

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

本申請實施例中提供了一種面向計算平臺的系統評估方法，通過根據計算機的非形式化描述語言轉化得到符號邏輯的等價公式；然后，根據符號邏輯的等價公式構建得到霍爾三元組模型；最后，根據霍爾三元組模型進行自動路徑測試，得到模型部分正確性結果；最后，根據霍爾三元組模型分析系統程序終止性，得到模型完全正確性結果。本申請將系統程序驗證問題轉化為邏輯推理問題，解決了現有技術的傳統評估系統檢測技術需要依賴人工逐句對系統進行驗證造成的評估結果不準確的問題。

技術領域

本申請屬于系統驗證與評估技術領域，具體地，涉及一種面向計算平臺的系統評估方法。

背景技術

隨著計算機系統、平臺的迅速發展，軟件系統的安全性、可靠性一直是網絡信息關注的焦點，隨著網絡技術的發展，各式各樣的軟件系統與硬件設備相結合，應用于不同的行業中。隨之而來的問題就是驗證系統的安全性和可靠性問題凸顯，在一些關鍵領域，如航空航天、醫療、國防等，軟件系統中任何微小的錯誤都可能引發重大損失。因此對系統進行有效分析驗證與評估及其重要。傳統評估系統檢測技術需要依賴人工逐句對系統進行驗證，導致自動化程度很低、耗時耗力、且人工驗證容易發生遺漏以及導致驗證及評估結果不夠準確各種問題。

霍爾邏輯是廣泛應用的程序驗證邏輯系統，用于對命令式語言程序進行推理驗證，其對程序的完全正確性證明分為兩步，首先證明程序的部分正確性，然后再證明程序的可終止性。

發明內容

本發明提出了一種一種面向計算平臺的系統評估方法，旨在解決現有技術的傳統評估系統檢測技術需要依賴人工逐句對系統進行驗證造成的評估結果不準確的問題。

根據本申請實施例的第一個方面，提供了一種面向計算平臺的系統評估方法，包括以下步驟：

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

根據符號邏輯的等價公式構建得到霍爾三元組模型；

根據霍爾三元組模型進行自動路徑測試，得到模型部分正確性結果；

根據霍爾三元組模型分析系統程序終止性，得到模型完全正確性結果。

可選地，非形式化描述語言通過采用一階邏輯對非形式化的計算機語言進行描述得到。

可選地，根據符號邏輯的等價公式構建得到霍爾三元組模型，具體包括：

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

可選地，根據霍爾三元組模型進行自動路徑測試中，具體包括：

通過符號執行的方式對霍爾三元組模型進行自動路徑測試。

可選地，通過符號執行的方式對霍爾三元組模型進行自動路徑測試，具體包括：

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

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

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

可選地，霍爾三元組模型不滿足部分正確性時，還包括輸出不滿足部分正確性原因。

可選地，根據霍爾三元組模型分析系統程序終止性中，具體包括：

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

可選地，啟發式搜索算法包括深度優先搜索算法或廣度優先搜索算法。

可選地，根據霍爾三元組模型分析系統程序終止性中，具體包括：