《嵌入式軟體正確性自動證明理論研究》是依託清華大學，由顧明擔任項目負責人的專項基金項目。
基本介紹
- 中文名：嵌入式軟體正確性自動證明理論研究
- 依託單位：清華大學
- 項目負責人：顧明
- 項目類別：專項基金項目
- 負責人職稱：教授
- 批准號：60553002
- 申請代碼：F0203
- 研究期限：2006-01-01 至 2008-12-31
- 支持經費：23（萬元）
項目摘要
嵌入式系統已經成為現代信息產業中重要和不可缺少的組成部分。隨著嵌入式系統複雜性的日益增加，設計出錯的可能性也持續增加。對於一個嵌入式系統，花費在驗證上的時間是花費在設計上時間的60%。如何有效保證設計的正確性是任何重大系統開發過程中所面臨的重要挑戰。形式化證明技術是保證系統正確性的一種強有力的方法。形式化證明技術是基於嚴格數學理論的證明理論與方法，它可以彌補傳統模擬的不足。狀態爆炸問題是有限狀態機
