《基於廣義符號軌跡賦值理論的模型檢測》是依託電子科技大學,由楊國武擔任醒目負責人的面上項目。
基本介紹
- 中文名：基於廣義符號軌跡賦值理論的模型檢測
- 依託單位：電子科技大學
- 項目類別：面上項目
- 項目負責人：楊國武
項目摘要,結題摘要,
項目摘要
廣義符號軌跡賦值（GSTE）是一種針對超大規模集成化電路設計的符號軌跡賦值的推廣。符號軌跡賦值在Intel、IBM和Motorola等公司得到成功的套用。廣義符號軌跡賦值可以驗證無限時間區間上的omega性質，在Intel得到成功套用。但它發展時間不長，還不成熟。本項目針對五個方面：GSTE中斷言圖之間的蘊涵關係，細化與反例的產生，GSTE與傳統模型檢驗的關係，軟硬體協同驗證，系統並發性質的驗證，進行研究。目標是豐富GSTE理論，實現基於這些理論的高效、準確的形式化驗證工具。基於語言的蘊涵關係可以轉換為傳統模型檢驗有限狀態機之間的蘊涵關係。基於模型的蘊涵關係可以通過求斷言圖的極大模型來判斷。如何在GSTE中引入SAT和按斷言圖作同步模擬是細化與產生反例的重要手段。比較GSTE檢驗方法與傳統模型檢驗方法的差別，融合它們的優點，設計高效的形式化驗證算法。同時建立軟硬體統一的形式化描述方法。
結題摘要
摘要：廣義符號軌跡賦值（GSTE）是一種針對超大規模集成化電路設計的符號軌跡賦值的推廣。廣義符號軌跡賦值在Intel、IBM和Motorola等公司得到成功的套用。我們研究了如下幾個方面：GSTE中斷言圖之間的蘊涵關係；細化與反例的產生；GSTE與傳統模型檢驗的關係；嵌入式系統的仿真；SAT問題完備算法的最佳化；SAT求解器和BDD的套用等等。我們比較了GSTE檢驗方法與傳統模型檢驗方法的差別，融合了它們的優點，設計出了高效的形式化驗證算法；我們豐富了GSTE理論，實現了基於這些理論的高效、準確的形式化驗證工具；同時，通過套用形式化的方法，我們驗證了一些混雜系統的特性，最佳化了生化系統中同步布爾網路求吸引子的算法等等。
