Title: 不可行路徑片段制導的線性混成自動機有界可達性檢驗及全局性質推導

       Hybrid Automata: On Bounded Reachability Checking Guided by Analysis of Infeasible Path Segments, and on Derivation of Global Properties

Speaker: 卜磊（南京大學）

         Lei Bu (Nanjing University, China)

         ( cs.nju.edu.cn/bulei )

Time: 8th January 2015, 09:30

Venue: Seminar Room (334), Level 3, Building 5, Institute of Software, CAS

Abstract:

混成自動機行為中離散跳轉與連續實時行為相交織，其狀態空間非常復雜難以驗證。即使是面向相對簡單的子類－線性混成自動機－相關問題業已被證明為不可判定。近年來相關工作主要在有界可達性驗證層面展開。傳統方法是將自動機在一定閾值內所有可能行為編碼成一組SMT約束，并調用SMT求解器進行求解。然而，隨著閾值數值的增大，對應SMT約束集的規模將快速增長從而限制了可驗證問題的規模。

應對此問題，本課題組提出了離散與連續分層考慮的新型有界可達性驗證算法。通過在離散層面尋找潛在路徑，在連續層面確認的形式控制單次驗證問題的規模。在此基礎上當連續層面發現相關路徑不可行時，定位其中不可行子路徑片段并將其反饋至離散層面對待驗證空間進行剪枝，從而高效完成相關驗證。更進一步，當相關不可行子路徑片段積累較多的時候，可以經常發現程序離散圖結構上已經不存在能連通起點至目標點的潛在路徑，在此情況下有界不可達性質可進一步被推廣到全局狀態空間。

Biography:

卜磊，現任南京大學計算機科學與技術系副教授，于2010年4月畢業于南京大學計算機科學與技術系，獲博士學位。主要研究領域是軟件工程與形式化方法，側重于模型檢驗技術，實時和混成系統，信息物理融合系統等方向。曾在美國CMU、UTD、歐盟FBK、日本NII、微軟亞洲研究院等科研機構進行訪學與合作研究。目前已在相關領域內重要期刊與會議如 RTSS、TPDS、CAV、FMSD、STTT、FMCAD、DATE、VMCAI、ICCPS 等上發表論文三十余篇。