發(fā)布時(shí)間：2019-03-25 21:22

【摘要】：混成系統(tǒng)是一類同時(shí)具有離散和連續(xù)行為的復(fù)雜系統(tǒng),被廣泛應(yīng)用于控制系統(tǒng)建模.針對(duì)其安全性需求,對(duì)不安全狀態(tài)進(jìn)行有界可達(dá)性驗(yàn)證,是保障系統(tǒng)安全的重要手段.然而,當(dāng)前技術(shù)所能處理的問(wèn)題規(guī)模和現(xiàn)實(shí)生活里的實(shí)際需要尚有一定的距離.特別是組合混成系統(tǒng)由于涉及到各個(gè)組件間的協(xié)作與同步,組合狀態(tài)空間快速爆炸,對(duì)其進(jìn)行驗(yàn)證具有極高的復(fù)雜性.為控制問(wèn)題的復(fù)雜度,一種面向路徑的可達(dá)性分析方法在前期工作中被提出用來(lái)對(duì)組合線性混成系統(tǒng)進(jìn)行有界可達(dá)性分析.該方法通過(guò)依次枚舉潛在路徑并進(jìn)行驗(yàn)證的方式,有效地提升了所能處理的問(wèn)題規(guī)模.當(dāng)面對(duì)復(fù)雜系統(tǒng)時(shí),上述面向路徑的檢測(cè)方法將會(huì)因?yàn)榇龣z測(cè)路徑數(shù)量的急劇上升而使得驗(yàn)證效率大幅降低,這也是模型檢驗(yàn)狀態(tài)空間爆炸問(wèn)題的一種體現(xiàn).為解決此問(wèn)題,本文提出了一種狀態(tài)空間約減技術(shù)以加速驗(yàn)證過(guò)程.當(dāng)一組路徑被判定為不可行時(shí),定位出導(dǎo)致其不可行的原因,得到一個(gè)組合不可行路徑片段.由于包含同樣片段的組合路徑一定不可行,因此在后續(xù)的路徑遍歷里只需要枚舉與檢驗(yàn)不包含組合不可行路徑片段的路徑,從而大幅減少需要檢驗(yàn)的路徑數(shù)量.此外,為了有效地規(guī)避此類組合路徑片段,我們?cè)O(shè)計(jì)了一種全新的基于SMT編碼的有界圖結(jié)構(gòu)遍歷方法.實(shí)驗(yàn)表明,該優(yōu)化技術(shù)大幅地提升了面向路徑有界可達(dá)性分析方法的性能,整體性能也超越了當(dāng)前最先進(jìn)的同類工具.
[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é)計(jì)算機(jī)軟件新技術(shù)國(guó)家重點(diǎn)實(shí)驗(yàn)室;江蘇省軟件新技術(shù)與產(chǎn)業(yè)化協(xié)同創(chuàng)新中心;
【基金】：國(guó)家重點(diǎn)基礎(chǔ)研究發(fā)展計(jì)劃(973)(批準(zhǔn)號(hào):2014CB340703) 國(guó)家自然科學(xué)基金(批準(zhǔn)號(hào):61561146394,61572249,61321491)資助項(xiàng)目
【分類號(hào)】：TP301.1

【相似文獻(xiàn)】

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

，

本文編號(hào)：2447328