《面向複雜行為場景的實時和混成系統模型檢驗技術研究》是依託南京大學，由卜磊擔任項目負責人的面上項目。
基本介紹
- 中文名：面向複雜行為場景的實時和混成系統模型檢驗技術研究
- 項目類別：面上項目
- 項目負責人：卜磊
- 依託單位：南京大學
項目摘要,結題摘要,
項目摘要
針對安全攸關套用領域中的實時和混成系統，採用模型檢驗技術驗證其是否滿足需求、擺脫缺陷十分重要和必要。然而實際套用中，這類系統的複雜性常常超出現有模型檢驗技術和工具的能力範圍，難以全局驗證。因此如何有效控制驗證中的複雜性、對系統的重要行為場景進行驗證成為亟待解決的重要問題。.通過對典型實時和混成系統的分析可以發現，其行為場景中的複雜性主要體現為：隨著系統組件間協同成為常態，組件互動帶來的交織與並發行為大量出現；隨著系統控制精確程度的不斷提升，大量非線性控制方程的引入導致系統行為空間難以求解；隨著系統與外界互動愈發密切，動態環境帶來的系統行為不確定性也迅速突顯。本項目針對上述複雜性導致的問題，採用基於反例子路徑定位的組合場景高效遍歷、可容忍誤差下的非線性場景快速求解、以及全周期覆蓋的動態場景線上驗證等方法進行研究，力爭控制驗證過程中的複雜性，設計高效算法，並研製可適應工業界套用需求的工具原型。
結題摘要
面向實施混成系統形式化驗證的複雜度挑戰，本項目從組合互動，非線性運算，不確定環境等複雜度角度進行研究，提出了基於組合IIS路徑定位的混成自動機驗證方法，基於帶參混成自動機建模語言的面向場景增量式線上驗證技術，基於無梯度最佳化的複雜非線性行為高效符號執行，面向事件驅動IoT的模型、規約、驗證與修復一體化驗證框架等技術。項目研究達到了預期的目標，已發表高質量學術論文30 篇，包括期刊論文 8 篇(分別發表在IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems、IEEE Transactions on Computer、ACM Transactions on Cyber-Physical Systems、中國科學、軟體學報等國內外重要期刊上)、以及ICSE、DATE、ISSTA、ICRA、SPIN等國際會議論文22篇。在上述研究結果的基礎上，課題組研發了一批工具原型，累計獲得授權中國發明專利7件，受理髮明專利 6 件，研發了包括混成自動機驗證工具BACH、HAT、事件驅動物聯網驗證工具MenShen、嵌入式代碼驗證工具BRICK、複雜代碼符號執行工具MLB等系列工具。在列控、航天等領域進行套用實踐，引起廣泛關注。項目執行期間，培養了博士生 3 人、碩士生 8 人，其中解定寶獲得中國計算機學會2017年度優秀博士論文，邢少鵬獲得中國計算機學會2018年度優秀大學生獎。項目負責人卜磊於2016年入選中國計算機學會青年人才發展計畫，獲2016年度Microsoft Research Asia Collaborative Research Award，2019年度NASAC青年軟體創新獎。
