基於混成計算的多核限界模型檢測

《基於混成計算的多核限界模型檢測》是依託大連理工大學,由孔維強擔任項目負責人的面上項目。

基本介紹

• 中文名：基於混成計算的多核限界模型檢測
• 依託單位：大連理工大學
• 項目類別：面上項目
• 項目負責人：孔維強

項目摘要

模型檢測作為提高軟體正確性的有效技術被廣泛研究，並於近年開始實際套用於軟體開發產業中。然而，現有技術和工具仍無法實現對大規模軟體系統正確性的驗證。本項目著眼於可處理較大規模驗證問題的限界模型檢測技術，為進一步提升其驗證能力和性能，提出新型的基於混成計算的多核限界模型檢測技術：將(無狀態)顯式探索算法融合於限界模型檢測，前者通過抽象狀態空間及抽取執行路徑為後者壓縮、拆分編碼公式、實現多核驗證；後者的SMT求解器提供不可滿足核心為前者縮減需探索的狀態空間。本項目凝練出實現該新型技術的5個關鍵科學問題，並逐一提出切實可行的研究方案。項目組在前期工作中已實現本項目的部分算法，實驗結果表明(CompJ,2014)，該技術的現有驗證能力和性能已優於知名限界模型檢測工具SAL，部分優於NuSMV。本項目的成功實施，有望顯著提升現有限界模型檢測技術的性能，為實現大規模軟體正確性驗證提供理論和工具支撐。

結題摘要

模型檢測作為提高軟體正確性的有效技術被廣泛研究，並於近年開始實際套用於軟體開發產業中。然而，現有技術和工具仍無法實現對大規模軟體系統正確性的驗證。本項目著眼於可處理較大規模驗證問題的限界模型檢測技術，為進一步提升其驗證能力和性能，提出新型的基於混成計算的多核限界模型檢測技術：將（無狀態）顯式探索算法融合於限界模型檢測，前者通過抽象狀態空間及抽取執行路徑為後者壓縮、拆分編碼公式、實現多核驗證；後者的SMT求解器提供不可滿足核心為前者縮減需探索的狀態空間。該算法同時融入插值抽象方法，可進一步擴展為非限界模型驗證。基於該算法，本項目發表學術論文14篇，其中CCF列表論文4篇，SCI論文5篇，EI論文14篇，培養軟體工程及形式化驗證領域青年教師3年，博士生3人，碩士生7人；另外，本項目基於該算法開發實現了模型檢測工具Garakabu2。實驗顯示，Garakabu2的驗證能力和性能已優於知名限界模型檢測工具SAL且部分優於NuSMV（部分安全屬性提升10倍以上），為實現大規模軟體正確性驗證提供了理論和工具支撐。