《面向時空約束的CPS協同機制的形式化建模與分析》是依託華東師範大學，由李欽擔任項目負責人的青年科學基金項目。
基本介紹
- 中文名：面向時空約束的CPS協同機制的形式化建模與分析
- 項目類別：青年科學基金項目
- 項目負責人：李欽
- 依託單位：華東師範大學
項目摘要,結題摘要,
項目摘要
信息物理融合系統（CPS）是由大量智慧型體組成的分散式系統，其中每個智慧型體都是一個具有計算、通信和控制能力的混成系統。由於每個智慧型體的可控資源和能力有限，系統任務的完成依賴於對各智慧型體行為的有效協同。與傳統軟體系統相比，CPS系統的需求規範具有顯著的時空特徵，每個智慧型體的行為也依賴於其相鄰時空的環境信息，CPS協同機制需要使智慧型體微觀行為的協同效果滿足系統的巨觀時空約束。如何對CPS的時空特徵和協同機制建立形式化模型，分析協同機制在時空性質下的行為，並在此基礎上驗證微觀協同行為滿足巨觀時空需求，是本項目擬解決的關鍵科學問題。本項目以UTP方法為基礎，提出一套面向CPS的時空性質表示方法，並在此基礎上提出針對時空約束的協同語言和語義模型，將巨觀時空約束和微觀協同行為統一到一個理論框架中；採用基於精化理論的形式化驗證技術，判定系統微觀協同行為是否滿足給定的巨觀時空需求。
結題摘要
與傳統軟體系統相比，信息物理融合系統（CPS）的需求規範具有顯著的時空特徵，每個智慧型體的行為也依賴於其相鄰時空的環境信息。CPS協同機制需要使系統與環境的互動行為的滿足給定的時空約束性質。本項目針對自動駕駛這一典型的CPS系統套用領域，圍繞面向時空約束的CPS系統協同機制的建模與驗證問題展開研究，具體研究內容和成果包括：（1）提出一種適合自動駕駛車輛環境的基於時空格線的時空約束描述語言，能夠描寫自動駕駛場景中同一時間點上不同位置之間的空間關係，並將不同時間的性質映射到時空格線中。（2）提出一種面向時空性質的CPS時空協同語言及其語義模型，該語義模型以代數語義為基礎，採用UTP理論推導出與其一致的指稱語義與操作語義模型，從而保證語義模型的正確性與兼容性，為CPS協同行為的分析驗證提供了堅實基礎。（3）在時空約束邏輯語言與協同行為建模語言的基礎上，對自動駕駛決策系統的安全性開展形式化建模與分析驗證。對自動駕駛時空環境信息建立抽象模型，採用機率模型對環境車輛決策的不確定性進行建模和預測，並在該不確定環境模型下對車輛自動駕駛決策行為的安全性進行定量分析，從而評估自動駕駛決策的安全性。本項目的研究共發表學術論文8篇，其中CCF A類期刊論文1篇，CCF B類期刊論文2篇，SCI二區期刊論文1篇，CCF C類會議論文2篇。共培養博士研究生2名，碩士研究生2名。
