基于組合IIS路徑抽取的組合線性混成系統有界可達性分析-中國科學

中國科學: 信息科學 2017 年 第47 卷 第3 期: 288–309

論文

基于組合 路徑抽取的組合線性混成系統有界

可達性分析優化

1 1 1,2 1,2 1,2

解定寶 周岳翔 卜磊 王林章 李宣東

1. 南京大學計算機軟件新技術國家重點實驗室, 南京 210023

2. 江蘇省軟件新技術與產業化協同創新中心, 南京 210023

* 通信作者. E-mail: bulei@

收稿日期: 2016–03–02; 接受日期: 2016–05–31; 網絡出版日期: 2016–09–14

國家重點基礎研究發展計劃(973) (批準號: 2014CB340703) 和國家自然科學基金 (批準號: 61561146394,

資助項目

摘要 混成系統是一類同時具有離散和連續行為的復雜系統 被廣泛應用于控制系統建模 針對其

安全性需求 對不安全狀態進行有界可達性驗證 是保障系統安全的重要手段 然而 當前技術所能

處理的問題規模和現實生活里的實際需要尚有一定的距離 特別是組合混成系統由于涉及到各個組

件間的協作與同步 組合狀態空間快速爆炸 對其進行驗證具有極高的復雜性 為控制問題的復雜

度 一種面向路徑的可達性分析方法在前期工作中被提出用來對組合線性混成系統進行有界可達性

分析 該方法通過依次枚舉潛在路徑并進行驗證的方式 有效地提升了所能處理的問題規模 當面對

復雜系統時 上述面向路徑的檢測方法將會因為待檢測路徑數量的急劇上升而使得驗證效率大幅降

低 這也是模型檢驗狀態空間爆炸問題的一種體現 為解決此問題 本文提出了一種狀態空間約減

技術以加速驗證過程 當一組路徑被判定為不可行時 定位出導致其不可行的原因 得到一個組合

不可行路徑片段 由于包含同樣片段的組合路徑一定不可行 因此在后續的路徑遍歷里只需要枚舉

與檢驗不包含組合不可行路徑片段的路徑 從而大幅減少需要檢驗的路徑數量 此外 為了有效地

規避此類組合路徑片段 我們設計了一種全新的基于 編碼的有界圖結構遍歷方法 實驗表明

該優化技術大幅地提升了面向路徑有界可達性分析方法的性能 整體性能也超越了當前最先進的同

類工具

關鍵詞 混成系統 有界模型檢驗 可達性分析 組合線性混成自動機 可滿足性 不可約不可解

子集

引言

混成系統 是一類同時具有離散和連續行為特征的復雜系統 被廣泛應用于工業

控制系統的建模 近年來 隨著軟件失效帶來的損失越來越大 人們對于系統的安全性要求越來越高

引用格式 解定寶 周岳翔 卜磊 等 基于組合 路徑抽取的組合線性混成系統有界可達性分析優化 中國科學 信息科學

? 《中國科學》雜志社

中國科學: 信息科學 第47 卷 第 3 期

尤其是安全攸關領域 幾乎已經到了零容忍的地步 模型檢驗 是一種可以自動化

發現系統錯誤的高效方法 其基本思想是遍歷系統模型的狀態空間 找出所有可能的錯誤 是保障系

統質量的重要手段 當前 混成自動機 是一種廣泛使用的混成系統建模語言 因

此 對混成自動機進行模型檢驗是相關領域的一個重要問題 由于混成自動機里離散與連續行為的混

雜交織 相應的模型檢驗問題十分困難 比如 即使是混成自動機的一個相對簡單的子類 線性混

總結

以上是生活随笔為你收集整理的岳翔南京大学计算机,基于组合IIS路径抽取的组合线性混成系统有界可达性分析-中国科学.PDF...的全部內容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網站內容還不錯，歡迎將生活随笔推薦給好友。