《混成系統模型檢驗套用技術研究》是依託南京大學，由卜磊擔任項目負責人的青年科學基金項目。
基本介紹
- 中文名：混成系統模型檢驗套用技術研究
- 項目類別：青年科學基金項目
- 項目負責人：卜磊
- 依託單位：南京大學
項目摘要,結題摘要,
項目摘要
混成系統的模型檢驗技術對實時系統質量保障具有重要意義。由於系統行為高度複雜，現有工作主要針對線性混成自動機的可達性檢驗，但可解決問題規模過小不足以滿足實際套用需要。同時，現有技術在非線性混成自動機可達性檢驗及混成自動機活性檢驗兩個重要套用領域所展開的工作頗為有限，亟待進一步研究。近年來，CPS系統廣泛興起，混成自動機作為其自然的建模語言，其模型檢驗問題顯得愈發重要。與一般嵌入式系統不同，CPS系統行為具有高度不確定性，因此傳統的離線建模驗證技術已無法滿足CPS系統的需要，如何應對此需求對CPS系統進行驗證也是一個重要科學問題。本課題將基於已有工作展開，以面向路徑可達性檢驗為基礎，數值約束技術為手段，多核技術為平台，服務於套用為目標，設計面向（非）線性混成自動機可達性，線性混成自動機活性的驗證算法，以此為基礎設計支持CPS系統的線上建模驗證框架，並結合典型CPS安全攸關係統進行示範性套用。
結題摘要
隨著實時、嵌入式系統乃至信息物理融合系統愈發廣泛地出現在人們生產生活的方方面面，如何保證相關係統的正確性，保證系統套用過程中不會出現危險是一項迫在眉睫的需求。在基金委的資助下，本項目從理論層混成自動機的多種性質模型檢驗技術、套用層信息物理融合系統的線上驗證技術以及信息物理融合系統底層無線感測網路的驗證、設計等技術進行了系統研究。提出了包括多技術深度融合的有界模型檢驗技術、基於不可行子路徑定位的有界結果全局拓展、基於等價遷移系統構造的混成系統活性、穩定性驗證、信息物理融合系統線上建模驗證等系列技術。相關技術在包括列控、醫療手術系統在內的信息物理融合系統仿真平台上進行實例研究，充分證明了其有效性。 項目實施3年來，發表錄用了高質量論文15篇，其中包括CCF－A論文三篇 （包括兩篇IEEE Transactions on Parallel and Distributed Systems, 一篇RTSS2014），CCF－B論文兩篇（包括DSN2013與Formal Methods in System Design），一級學報《中國科學》、《軟體學報》等。此外，在CPS系統領域旗艦會議ICCPS上連續多年發表了包括Regular、Poster、Demo、WIP在內的系列文章。同時項目組還出版譯著一部。 本項目申請國家發明專利8項，獲取軟體著作權6項。本課題開發了面向混成自動機有界模型檢驗工具BACH系列，面向CPS系統線上建模與驗證BACH Online系列， 基於遷移系統的混成自動機活性、穩定性分析工具HVT系列等多項工具。相關工具線上免費發布，引起廣泛關注，下載次數過百，其中不乏美國卡耐基梅隴，加州大學伯克利分校等頂級學府的研究人員。本工作所取得成果取得廣泛影響， 相關工作在國內外受邀報告多次，包含美國卡耐基梅隆大學、日本國立情報學研究所、新加坡工業設計大學、中國科學院軟體所、江蘇省計算機協會年會等。 特別值得一提的是本工作所提出的混成自動機有界模型檢驗及線上建模驗證工作在國際一流會議FM2014上進行了半天的專題Tutorial報告，這也充分證明了本工作的被認可程度。
