[發明專利]基于機器學習的循環不變式自動生成方法

在審

• 申請號: 201910630164.5
• 申請日: 2019-07-12
• 公開（公告）號: CN110377513A
• 公開（公告）日: 2019-10-25
• 發明（設計）人: 路紅;史玉石
• 申請（專利權）人: 南京理工大學紫金學院
• 主分類號: G06F11/36
• 分類號: G06F11/36
• 代理公司: 南京知識律師事務所 32207
• 代理人: 李吉寬

本發明公開了基于機器學習自動生成循環不變式的方法。首先對含循環語句的計算機程序依據一定的算法得到循環語句的后置條件，構造循環語句對應的Hoare三元組；然后依據循環語句的前置條件隨機生成測試數據，以這些測試數據為循環變量的初始值運行循環語句，收集程序狀態，構造數據集SV；對數據集SV中的每一組數據依據Hoare三元組進行分類標注形成分類數據集；利用KSVM算法對所收集的分類數據集進行分類，生成候選循環不變式；利用反證法對生成的候選不變式進行有效性驗證，得到經驗證的有效循環不變式。本發明實現了面向可運行的C程序的自動生成循環不變式，且支持生成提供形式更加豐富的循環不變式，能夠大大減少形式化驗證中循環語句自動驗證的工作量。

技術領域

本發明屬于軟件工程、自動驗證、形式化方法技術領域，涉及一種循環不變式自動生成方法。

背景技術

軟件作為當今信息化社會的重要基礎設施，已廣泛應用于能源、交通、通信、金融和國防等安全攸關領域中。然而，隨著軟件集成程度的提高和軟件系統結構的日益復雜，各類軟件的高可信性質越來越不能保證。軟件驗證以邏輯和數學為基礎，支持軟件進行嚴格的形式規約和驗證，是確保軟件可信性的一種有效措施。軟件驗證的目標是證明程序在任何執行路徑下均滿足一定的形式化規約，即程序在確定的條件下執行結束后便可滿足一定的要求。軟件驗證的一般步驟是針對待驗證的程序撰寫形式化規約(如前置條件、后置條件和循環不變式)，然后利用自動驗證工具或交互式定理證明器驗證給定程序是否滿足所撰寫的形式化規約。根據所使用的驗證工具不同，可將形式化驗證方法分為人工撰寫證明腳本和自動化驗證兩類。人工撰寫形式化證明腳本方法即驗證者利用Isabelle、Coq和HOL4等交互式定理證明器，依據待驗證程序運行環境建立形式化模型，根據其滿足的屬性建立形式化規約，并在交互式定理證明器中完成推理驗證，其證明開銷較大。

為了提高驗證效率、簡化驗證難度，出現了Z3、Danfy和Why3等自動化驗證工具。運用自動化驗證工具對代碼量較少的程序進行驗證，無需驗證者撰寫大量證明腳本，僅需按照自動化驗證工具的規范撰寫待驗證程序的形式化規約，即可快速得到程序是否正確的驗證結果。然而，為程序提供合適的形式化規約，尤其是循環不變式，需要驗證者依據對程序的深刻理解進行手工撰寫，這對于驗證者來說是一項任務繁重的工作任務且容易出現錯誤。

發明內容

本發明所要解決的問題是提供一種基于機器學習的方法實現面向可運行的計算機程序的自動生成循環不變式，以克服自動驗證過程需要手工撰寫循環不變式的困難，縮短驗證周期和避免手工撰寫循環不變式出現的錯誤問題。

為此目的，本發明提供的基于機器學習自動生成循環不變式的方法，包括以下步驟，

步驟一，對含循環語句的計算機程序，如C程序，依據所設計的自動生成后置條件的算法得到循環語句的后置條件，構造計算機程序中循環語句對應的Hoare三元組；

步驟二，依據循環語句的前置條件隨機生成測試數據，以這些測試數據為循環變量的初始值運行循環語句，收集程序狀態，從而構造數據集SV；

步驟三，對數據集SV中的每一組數據，依據Hoare三元組所定義的關系進行分類標注形成分類數據集；

步驟四，利用所設計的核支持向量機KSVM(Kernel Support Vector Machine)算法對所收集的分類數據集進行分類，從而生成候選循環不變式；

步驟五，利用反證法對生成的候選不變式進行有效性驗證，得到經驗證的有效循環不變式。

進一步，上述步驟一中，其目標是實現對程序中循環語句后置條件的自動生成，所述含循環語句的程序是具有前置條件、單層循環且循環變量是可歸納類型，以便通過邊界值分析法計算出循環次數并結合前置條件生成后置條件。