《基於假設/保證自動推理的組合驗證研究》是依託清華大學，由賀飛擔任項目負責人的青年科學基金項目。
基本介紹
- 中文名：基於假設/保證自動推理的組合驗證研究
- 依託單位：清華大學
- 項目負責人：賀飛
- 項目類別：青年科學基金項目
項目摘要,結題摘要,
項目摘要
狀態空間爆炸問題是制約模型檢測套用的主要問題。基於假設/保證（Assume/Guarantee，簡稱A/G）規則的自動推理框架被認為是最有前途的組合驗證方法學之一，具有非常重要的理論與套用價值。區別於一般的A/G組合驗證，該框架能夠完全自動化。該技術的研究在國際上仍是嶄新且富有挑戰性的，有很多問題尚未解決。本課題擬對該技術的三個基本問題展開研究，即A/G自動推理框架、模型自動分解算法和符號化模型檢測算法。此外，本課題還將從套用角度對該技術進行探討，將基於接口自動機對該理論進行擴展，並將其套用到典型嵌入式系統的驗證之中。
結題摘要
狀態空間爆炸問題是制約模型檢測套用的主要問題。基於假設/保證（Assume/Guarantee，簡稱A/G）規則的自動推理框架被認為是最有前途的組合驗證方法學之一，具有非常重要的理論與套用價值。本課題對該技術的三個基本問題展開研究，即A/G自動推理框架、模型自動分解算法和符號化模型檢測算法。主要研究內容包括：模型自動分解算法、A/G自動推理框架、基於其他自動機的擴展、符號化驗證算法、符號化驗證引擎等。本項目達到並部分超過了預期的目標，至今已發表學術論文8篇（包括IEEE Transactions on Computers 2篇，本領域頂級會議CAV 1篇）。設計並實現了一個面向構件化嵌入式系統的模型檢測工具VCS，並且在門倉控制系統、多功能車輛匯流排控制器（MVBC）等典型嵌入式系統中進行了套用。
