《基於UTP的混成建模語言的理論研究》是依託華東師範大學，由趙涌鑫擔任項目負責人的青年科學基金項目。
基本介紹
- 中文名：基於UTP的混成建模語言的理論研究
- 項目類別：青年科學基金項目
- 項目負責人：趙涌鑫
- 依託單位：華東師範大學
項目摘要,結題摘要,
項目摘要
信息物理融合系統Cyber-Physical System（簡稱CPS）是近些年來學術研究的熱點領域之一。其主要特徵表現為物理進程和計算進程的深度融合，廣度互動。如何保證信息物理融合系統的正確性業已成為國內外工業界和學術界的難題之一。要保證CPS系統的正確性首先要解決的問題就是將物理進程和計算進程集中在同一框架下做分析推理。本項目致力於為CPS提供新的混成建模語言，深入研究物理進程和計算進程的互動機制，並建立具有嚴密數學基礎的指稱語義模型和代數語義模型，構建相應的代數演算系統和代數規範型。在此基礎上，利用代數重寫規則，發展有效的代數精化理論和程式分解理論，從而為CPS的分析、設計、實現和驗證提供堅實的理論基礎。
結題摘要
混成系統是近些年來學術研究的熱點領域之一，其主要特徵表現為物理進程和計算進程的深度融合，廣度互動，混成系統的異構性、複雜的時間約束性、一定的時間可預測性、更高的安全性以及互動的複雜性和不可預測性，給這類系統的描述、設計、分析和驗證帶來了巨大的挑戰。如何保證信息物理融合系統的正確性業已成為國內外工業界和學術界的難題之一。本項目發展了一種混成系統的建模語言和基於事件的建模方法，引進了when型程式和Until型程式分別用來處理離散行為變遷和連續模式切換，形式化地描述了混成系統的行為和性質，提出了混成建模語言的若干語義模型，我們首先以公理化的方法描述基本原子反應和組合運算元的含義，探討混成建模語言的規範型，揭示了混成系統行為的基本模式，所有不同語法形式的混成程式都可以利用代數規則轉化為規範型，從而將程式行為的語義分析轉化為程式規範型的語法分析，為混成系統的分析和驗證提供堅實的語義基礎。研究了混成系統的中斷機制，構造中斷程式的描述語言和語義模型，發展了混成系統中斷機制的分析方法和驗證技術，如：中斷程式的總體執行時間、不同中斷類型的中斷點檢查以及中斷次數統計。運用提出的建模技術，對自動駕駛、車聯網、多智慧型體等實例系統進行建模和分析，為其他類型混成系統的分析和驗證提供了參考和思路。該項目共發表學術論文12篇，其中SCI論文4篇，EI論文8篇，CCF B類論文3篇，CCF C類論文4篇。
