《微分半代數程式模型的等價及等價譜系》是依託北京交通大學，由吳盡昭擔任項目負責人的面上項目。
基本介紹
- 中文名：微分半代數程式模型的等價及等價譜系
- 項目類別：面上項目
- 項目負責人：吳盡昭
- 依託單位：北京交通大學
項目摘要,結題摘要,
項目摘要
行為等價是軟體程式設計與驗證分析的基礎。微分半代數混雜系統是近年來出現的新型形式化程式刻畫模型，在工程技術領域具有極其廣泛的套用。針對微分半代數程式模型，目前較為完善的等價理論還沒有建立起來。本項目通過並發理論、微分代數符號計算以及符號與數值混合計算方法的交叉、融合與套用研究，採用帶微分半代數方程組狀態轉移標記的混雜變遷系統，系統地構建微分半代數程式模型的行為等價理論。具體包括，（1）等價的定義：基於微分半代數程式模型的各類動態行為特徵，建立模型的線性與分支時間等價以及相應的帶誤差的近似等價關係；（2）等價的判定：研究微分半代數程式模型各類等價關係的可判定性，並實現帶誤差但誤差可控的近似等價計算方法；（3）等價間的關係：通過等價概念之間粗糙程度的比較關係，構建微分半代數程式模型的等價譜系。在實證示範和實際套用方面，探索在軌道高速列車運行控制軟體系統設計與驗證分析中的套用。
結題摘要
微分半代數混雜系統是近年來出現的一種刻畫程式的形式化模型，在工程技術領域內具有極其廣泛的套用。在軟體程式設計與驗證分析方面，行為等價和等價譜系研究是一項重要的基礎工作。本項目通過並發理論、微分半代數符號計算以及符號與數值混合計算方法的交叉、融合，採用帶微分半代數方程組狀態遷移標記的混雜變遷系統，系統地構建了微分半代數程式模型的行為等價理論，構建了包含不同粗糙程度行為等價的等價譜系。項目解決或部分解決了以下幾個問題：（1） 等價的定義：基於微分半代數程式模型的各類動態行為特徵，建立了模型的線性與分支時間等價以及相應的帶誤差的近似等價關係；（2） 等價的判定：利用微分半代數符號計算以及符號與數值混合計算的方法，研究了微分半代數程式模型的各類等價關係的可判定性問題，併合理地實現了部分帶誤差但誤差可控的近似等價計算方法；（3） 等價間的關係：通過比較各等價概念之間的粗糙程度，構建了微分半代數程式模型的等價譜系；（4） 行為性質的保持：通過構建微分半代數程式模型的邏輯推理系統，研究了若干重要行為性質在各等價關係下的保持情況。在實證示例和實際套用方面，探索微分半代數程式模型在列車運行控制系統設計與驗證分析以及積體電路設計驗證中的套用。已發表或錄用論文33篇，出版著作1本，組織了一場國際會議。
