《基於歸納不變式的模型檢測研究》是依託清華大學，由賀飛擔任項目負責人的面上項目。
基本介紹
- 中文名：基於歸納不變式的模型檢測研究
- 依託單位：清華大學
- 項目負責人：賀飛
- 項目類別：面上項目
項目摘要,結題摘要,
項目摘要
對於一些安全攸關係統，必須藉助於形式化方法才能保證其正確性和可靠性。作為最成功的形式化驗證方法之一，模型檢測技術在工業界（尤其是硬體界）得到了廣泛的套用。將模型檢測技術套用於軟體系統驗證，面臨的最大問題是狀態空間爆炸。基於歸納不變式的模型檢測技術被認為是應對該問題的有效途徑之一。該技術的研究在國際上仍是嶄新且富有挑戰性的，具有非常重要的理論與套用價值。本課題擬對該技術幾個關鍵問題展開研究，包括：歸納不變式自動生成技術，基於歸納不變式的模型檢測技術，和基於歸納不變式的組合驗證技術。以此為基礎設計支持複雜構件化系統的模型檢測工具，並在典型嵌入式系統中進行套用。
結題摘要
對於一些安全攸關係統，必須藉助於形式化方法才能保證其正確性和可靠性。作為最成功的形式化驗證方法之一，模型檢測技術在工業界（尤其是硬體界）得到了廣泛的套用。本課題針對模型檢測的狀態空間爆炸問題，研究將歸納不變式套用到模型檢測技術之中。首先，提出了一種基於學習的歸納不變式生成方法；其次，基於歸納不變式實現了一種面向安全屬性的驗證方法；再次，系統全面的研究了基於學習的組合驗證方法，並將其擴展到機率系統與回歸驗證。最後，基於上述成果，開發了模型檢測工具Beagle和軟體驗證工具Ceagle，並在某航空發動機控制軟體系統中進行套用。
