《基於 SAT 的擴展時序邏輯的符號化模型檢驗》是依託中國人民解放軍國防科技大學，由劉萬偉擔任項目負責人的青年科學基金項目。
基本介紹
- 中文名：基於 SAT 的擴展時序邏輯的符號化模型檢驗
- 項目類別：青年科學基金項目
- 項目負責人：劉萬偉
- 依託單位：中國人民解放軍國防科技大學
中文摘要,結題摘要,
中文摘要
隨著計算機軟硬體設計複雜性的日益增加，系統設計和實現的正確性越來越難以得到保證。模型檢驗方法被證明為行之有效的系統正確性驗證手段。模型檢驗問題所遇到的瓶頸在於目標狀態空間的爆炸，它限制了模型檢驗工具所能處理問題的規模。符號化模型檢驗能夠有效的縮減模型檢驗的效率，提高其規模。其中，基於 SAT 的符號化模型檢驗算法能力尤為突出。. 目前，具有完備 omega-正規性質表達能力的模型檢驗問題越來越受到廣泛關注，它們中的某些已經成為工業界的規約標準。擴展時序邏輯（ETL）是這一類語言的公共原型。本課題擬研究三類擴展時序邏輯基於 SAT 的符號模型檢驗算法（包括 BMC 算法和 UBMC 算法），並實現其相關工具
結題摘要
模型檢驗技術是計算機軟硬體系統正確性保障的重要手段，該技術的主要套用平靜在於“狀態空間爆炸問題”。符號化技術被證明是一種行之有效 的降低模型檢驗時空開銷的手段。同時，伴隨著 SAT 求解的技術突破,其套用逐步擴展到符號化模型檢驗領域。此外，正規性質的驗證問題由其理論意義和套用價值的重要性，使得其在模型檢驗領域一度受到廣泛關注。本項目的主要關注點在於基於 SAT 的各類線性框架下時序邏輯的符號化模型檢驗問題。主要工作包括： 1. 以擴展時序邏輯（ETL）為典型用例，給出了基於 SAT 的擴展時序邏 輯的模型檢驗算法及一般框架。 2. 針對線性時序邏輯符號化模型檢驗問題，提出了“保持反例的規約化簡”技術（CePRe）， 該技術可有效降低符號化模型檢驗時空開銷。 3. 給出了語法與語義相結合的 LTL 限界模型檢驗編碼算法，該算法能夠 有效的提高編碼效率，並能夠方便的計算完備閾值。 4. 對於非限界模型檢驗,給出了可並行實現的雙向 PDR 算法，可提高驗證效率。 5. 同時針對“模型等價性檢查”、”基於重寫的運行時驗證” 以及 “機率模型檢驗算法最佳化”等問題進行了相關研究。 6. 上述主要算法集成在兩個工具 ENuSMV（Ver1.2）以及 Reach 中，並均已開源發布。 5. 同時針對“模型等價性檢查”、”基於重寫的運行時驗證”以及“機率模型 檢驗算法最佳化”等問題進行了相關研究。 6. 上述主要算法集成在兩個工具ENuSMV(Ver1.2)以及Reach中，並 均已開源發布。
