混成系統設計演算

《混成系統設計演算》是依託中國人民解放軍國防科技大學，由王戟擔任項目負責人的青年科學基金項目。

基本介紹

• 中文名：混成系統設計演算
• 項目類別：青年科學基金項目
• 項目負責人：王戟
• 依託單位：中國人民解放軍國防科技大學
• 負責人職稱：研究員
• 申請代碼：F0203
• 研究期限：1997-01-01 至 1999-12-31
• 批准號：69603010
• 支持經費：10（萬元）

中文摘要

本項目在研究比較國內外混合系統開發方法的基礎上，從混合系統的形式模型和語義、形式驗證方法和支撐工具等方面對混合系統的形式化方法開展了研究，主要成果有：提出了一種混合系統模型設計語言及其混合變遷語義，並提出了一個基於三值區間的模型檢驗算法；利用超密時段演算，以混合通訊順序進程描述語言為基礎，提出混合系統的超密時段語義；提出一種帶next運算元的時段演算用以推理超密計算下的動作和事件；提出了分布實進機率系統定性和定量驗證的模型檢驗算法；提出了一種基於樹自動機的高效模型檢驗算法；在PVS上設計並實現了一個支持包括時段演算在內的區間邏輯推理的實時系統驗證工具；提出了區間邏輯的標記相繼式演算；等等。