【摘要】：混成系統(tǒng)是一類同時具有離散和連續(xù)行為的復(fù)雜系統(tǒng),被廣泛應(yīng)用于控制系統(tǒng)建模.針對其安全性需求,對不安全狀態(tài)進行有界可達性驗證,是保障系統(tǒng)安全的重要手段.然而,當(dāng)前技術(shù)所能處理的問題規(guī)模和現(xiàn)實生活里的實際需要尚有一定的距離.特別是組合混成系統(tǒng)由于涉及到各個組件間的協(xié)作與同步,組合狀態(tài)空間快速爆炸,對其進行驗證具有極高的復(fù)雜性.為控制問題的復(fù)雜度,一種面向路徑的可達性分析方法在前期工作中被提出用來對組合線性混成系統(tǒng)進行有界可達性分析.該方法通過依次枚舉潛在路徑并進行驗證的方式,有效地提升了所能處理的問題規(guī)模.當(dāng)面對復(fù)雜系統(tǒng)時,上述面向路徑的檢測方法將會因為待檢測路徑數(shù)量的急劇上升而使得驗證效率大幅降低,這也是模型檢驗狀態(tài)空間爆炸問題的一種體現(xiàn).為解決此問題,本文提出了一種狀態(tài)空間約減技術(shù)以加速驗證過程.當(dāng)一組路徑被判定為不可行時,定位出導(dǎo)致其不可行的原因,得到一個組合不可行路徑片段.由于包含同樣片段的組合路徑一定不可行,因此在后續(xù)的路徑遍歷里只需要枚舉與檢驗不包含組合不可行路徑片段的路徑,從而大幅減少需要檢驗的路徑數(shù)量.此外,為了有效地規(guī)避此類組合路徑片段,我們設(shè)計了一種全新的基于SMT編碼的有界圖結(jié)構(gòu)遍歷方法.實驗表明,該優(yōu)化技術(shù)大幅地提升了面向路徑有界可達性分析方法的性能,整體性能也超越了當(dāng)前最先進的同類工具.
[Abstract]:Hybrid system is a kind of complex system with both discrete and continuous behavior. It is widely used in the modeling of control systems. According to its security requirements, it is an important means to ensure the security of the system to verify the reachability of the insecure state. However, there is still a certain distance between the scale of the problems that the current technology can deal with and the actual needs of the real life. Especially, it is very complicated to verify the combinatorial hybrid system because it involves the cooperation and synchronization among the components and explodes rapidly in the combinatorial state space. In order to control the complexity of the problem, a path-oriented reachability analysis method was proposed in the previous work to analyze the bounded reachability of composite linear hybrid systems. By enumerating and validating the potential paths in turn, this method can effectively increase the size of the problem that can be dealt with. When faced with complex systems, the above-mentioned path-oriented detection methods will greatly reduce the verification efficiency due to the sharp increase in the number of paths to be detected, which is also a manifestation of the state space explosion problem of model checking. In order to solve this problem, a state space reduction technique is proposed to accelerate the verification process. When a group of paths is determined to be infeasible, the reasons leading to its infeasibility are located, and a combined infeasible path fragment is obtained. Since a combinatorial path containing the same fragment must not be feasible, it is necessary to enumerate and verify the paths that do not contain the combinatorial infeasible path fragment in the subsequent path traversal, thus greatly reducing the number of paths that need to be checked. In addition, in order to avoid this kind of combinatorial path fragments effectively, we design a new traversal method of bounded graph structure based on SMT coding. The experimental results show that the optimization technique greatly improves the performance of the path-oriented bounded reachability analysis method, and the overall performance exceeds the most advanced tools of the same kind.
【作者單位】： 南京大學(xué)計算機軟件新技術(shù)國家重點實驗室;江蘇省軟件新技術(shù)與產(chǎn)業(yè)化協(xié)同創(chuàng)新中心;
【基金】：國家重點基礎(chǔ)研究發(fā)展計劃(973)(批準(zhǔn)號:2014CB340703) 國家自然科學(xué)基金(批準(zhǔn)號:61561146394,61572249,61321491)資助項目
【分類號】：TP301.1

【相似文獻】

相關(guān)期刊論文 前10條

1 李浪;李仁發(fā);李肯立;姚鳳娟;;混成系統(tǒng)研究綜述[J];計算機應(yīng)用研究;2008年08期

2 侯建民,鄭滔,樊曉聰,李宣東,鄭國梁;線性混成系統(tǒng)的參數(shù)分析[J];計算機學(xué)報;1999年06期

3 范雙南;;基于時間序列分析的混成系統(tǒng)可靠性評價方法[J];福建電腦;2011年03期

4 鄒進;林望;羅勇;曾振柄;;基于多面體包含的非線性混成系統(tǒng)可達性分析[J];計算機應(yīng)用;2013年05期

5 卜磊;解定寶;;混成系統(tǒng)形式化驗證[J];軟件學(xué)報;2014年02期

6 喬磊;齊驥;龔育昌;;一種支持可重構(gòu)混成系統(tǒng)的操作系統(tǒng)設(shè)計與實現(xiàn)[J];計算機學(xué)報;2009年05期

7 趙劍;歐陽丹彤;王曉宇;張立明;;混成系統(tǒng)的分布式診斷方法[J];吉林大學(xué)學(xué)報(工學(xué)版);2012年06期

8 肖娟;;混成系統(tǒng)的形式驗證[J];長沙通信職業(yè)技術(shù)學(xué)院學(xué)報;2008年01期

9 葉林;湯瀑;郭立鵬;張亮;;基于混成系統(tǒng)的物聯(lián)網(wǎng)服務(wù)建模與驗證[J];小型微型計算機系統(tǒng);2013年12期

10 閻安,唐稚松;基于 XYZ/ E的混成系統(tǒng)(英文)[J];軟件學(xué)報;2000年01期

相關(guān)會議論文 前1條

1 任雁;田婕;孫輝;周永;;混成系統(tǒng)測試研究綜述[A];2011年通信與信息技術(shù)新進展——第八屆中國通信學(xué)會學(xué)術(shù)年會論文集[C];2011年

相關(guān)博士學(xué)位論文 前5條

1 解定寶;混成系統(tǒng)有界模型檢驗優(yōu)化技術(shù)研究[D];南京大學(xué);2016年

2 林望;基于符號數(shù)值混合計算的混成系統(tǒng)可信分析與驗證研究[D];華東師范大學(xué);2013年

3 趙劍;混成系統(tǒng)基于模型診斷的若干問題研究[D];吉林大學(xué);2012年

4 孔輝;基于歸納不變式的混成系統(tǒng)安全性驗證[D];清華大學(xué);2013年

5 李廣元;LTLC：面向?qū)崟r與混成系統(tǒng)的連續(xù)時序邏輯[D];中國科學(xué)院軟件研究所;2001年

相關(guān)碩士學(xué)位論文 前7條

1 楊陽;基于深度優(yōu)先搜索的混成系統(tǒng)有界可達性分析[D];南京大學(xué);2013年

2 蔣慧;基于遷移系統(tǒng)語義的線性混成系統(tǒng)分析[D];南京大學(xué);2013年

3 李國拯;基于組合形式規(guī)范的混成系統(tǒng)形式化驗證方法研究[D];南京航空航天大學(xué);2015年

4 鄒進;非線性混成系統(tǒng)的可達性分析[D];溫州大學(xué);2013年

5 李倩;基于形式化方法的混成系統(tǒng)安全性檢驗[D];華東師范大學(xué);2015年

6 錢宇清;Hybrid AADL：混成系統(tǒng)體系結(jié)構(gòu)分析與設(shè)計語言[D];華東師范大學(xué);2014年

7 錢磊;信息物理融合系統(tǒng)的形式化建模與討論[D];華東師范大學(xué);2013年

，

本文編號：2447328