基於定理證明的可信嵌入式軟體建模與驗證平台研究

《基於定理證明的可信嵌入式軟體建模與驗證平台研究》是依託清華大學，由顧明擔任項目負責人的重大研究計畫。

基本介紹

• 中文名：基於定理證明的可信嵌入式軟體建模與驗證平台研究
• 依託單位：清華大學
• 項目負責人：顧明
• 項目類別：重大研究計畫
• 批准號：90718039
• 申請代碼：F0202
• 負責人職稱：教授
• 研究期限：2008-01-01 至 2010-12-01
• 支持經費：250（萬元）

項目摘要

隨著信息技術的發展，嵌入式系統在眾多行業中得到廣泛使用。為了避免由於嵌入式軟體系統本身缺陷或系統中微小的錯誤而導致系統整體崩潰，嵌入式軟體系統的可信性得到了廣泛關注。本課題的目標是以定理證明為框架，結合模型檢測方法，針對嵌入式軟體自身特性，構建基於定理證明的可信嵌入式軟體設計過程中建模與驗證平台，實現系統級可信屬性的驗證。為此，本課題擬開展嵌入式軟體建模理論及說明語言、基於組合驗證的模型分解技術、