《混合系統的形式驗證》是依託西安電子科技大學，由段振華擔任項目負責人的面上項目。
基本介紹
- 中文名：混合系統的形式驗證
- 項目類別：面上項目
- 項目負責人：段振華
- 依託單位：西安電子科技大學
- 批准號：60373103
- 申請代碼：F0214
- 負責人職稱：教授
- 研究期限：2004-01-01 至 2006-12-31
- 支持經費：24（萬元）
中文摘要
建立混合系統的計算模型；基於這個模型，建立一個時序邏輯系統，它既是系統刻畫語言又是系統規範語言。建立一個可視化的系統刻畫語言，並建立從這個語言到時序邏輯語言的轉換規則；建立時序邏輯語言的模型理論，檢驗可滿足性的判定，探索可判定子類的分類，發展該時序邏輯的算法驗證方法，包括模型檢查。建立該時序邏輯的證明系統，發展基於該系統的演繹法對混合系統進行形式驗證的規則和方法。建立一個層次的刻畫語言，用以在不同抽象級上表達混合系統，並逐步求精得到系統的描述。由於HM和HPTL是基礎，該研究是源頭性的，它具有很重要的意義。
