本文關(guān)鍵詞：混成系統(tǒng)有界模型檢驗優(yōu)化技術(shù)研究

  更多相關(guān)文章： 混成系統(tǒng) 線性混成自動機 非線性混成自動機 有界可達性檢驗 面向路徑可達性檢驗 基于SAT的路徑遍歷 Satisfiability Modulo Theories 線性時序邏輯 不可約不可解子集

【摘要】：混成系統(tǒng)是一類包含連續(xù)和離散行為的復(fù)雜系統(tǒng),被廣泛應(yīng)用于工業(yè)控制系統(tǒng)的建模,混成自動機是當(dāng)前其主流建模語言,混成自動機的有界模型檢驗是保障系統(tǒng)可靠性和安全性的重要途徑�；斐勺詣訖C有界模型檢驗的基本思想是通過SMT (Satisfiability Modulo Theories)技術(shù)對系統(tǒng)在閾值內(nèi)的行為進行編碼并求解,以檢驗系統(tǒng)是否滿足相關(guān)性質(zhì)。但是由于這種方法需要提前一次性計算出系統(tǒng)閡值內(nèi)所有的狀態(tài)空間,如此高的計算復(fù)雜性限制了其能處理的系統(tǒng)規(guī)模,難以應(yīng)用到工業(yè)界的實際系統(tǒng)。另一種解決問題的思路是將整個系統(tǒng)的有界模型檢驗問題分解成系統(tǒng)內(nèi)各路徑的檢驗問題來控制單次驗證的復(fù)雜度,在此基礎(chǔ)上遍歷系統(tǒng)內(nèi)路徑完成整個系統(tǒng)的有界模型檢驗。盡管這種面向路徑的有界模型檢驗途徑有效地提升了可檢驗的系統(tǒng)規(guī)模,但是當(dāng)面對工業(yè)界的大規(guī)模系統(tǒng)時仍然需要有效的優(yōu)化技術(shù)進一步控制解決問題的復(fù)雜性。本文基于混成系統(tǒng)面向路徑的有界模型檢驗途徑,針對有界可達性問題研究相關(guān)優(yōu)化技術(shù),在狀態(tài)空間約減、組合系統(tǒng)遍歷優(yōu)化、基于局部驗證推導(dǎo)全局性質(zhì)、非線性系統(tǒng)檢驗等四個方面取得以下結(jié)果：·提出了SAT-HS-LP聯(lián)合反饋制導(dǎo)的狀態(tài)空間約減方法。首先基于SAT編碼模型的離散結(jié)構(gòu)有向圖并求解,盡量在早期發(fā)現(xiàn)不可行路徑；然后針對在路徑可達性檢驗過程中確定的不可行路徑,利用不可約不可解子集(Irreducible Infeasible Subset, IIS)技術(shù)從中定位出不可行子路徑片段,在后續(xù)的搜索中只需枚舉不包含相關(guān)不可行路徑片段的路徑進行檢驗,從而約減了狀態(tài)空間。實驗顯示,該方法大幅度地提升了面向路徑有界可達性檢驗的性能和規(guī)模。·針對組合線性混成系統(tǒng),提出了一種基于組合IIS路徑抽取的遍歷優(yōu)化方法�；赟MT編碼模型的離散結(jié)構(gòu)有向圖并求解,從而在組合系統(tǒng)的圖結(jié)構(gòu)上快速枚舉出符合同步語義的路徑組；依據(jù)組合自動機的同步語義,從不可行路徑組里抽取不可行組合路徑片段,從而在后續(xù)路徑遍歷過程中規(guī)避包含這些片段的路徑。實驗顯示該方法提高了組合系統(tǒng)可達性檢驗的效率�！ぬ岢隽艘环N基于有界可達性檢驗結(jié)果推導(dǎo)出系統(tǒng)全局性質(zhì)的途徑。在有界可達性檢驗的過程中,會不斷地收集到不可行子路徑片段,當(dāng)相關(guān)不可行子路徑片段積累較多的時候,可能導(dǎo)致程序離散圖結(jié)構(gòu)上已經(jīng)不存在能連通起點至目標(biāo)點的潛在路徑,在此情況下有界不可達性質(zhì)可以進一步被推廣到全局狀態(tài)空間,并可以通過基于線性時序邏輯(Linear Temporal Logic, LTL)模型檢驗的方法來完成對該類問題的自動證明。·針對非線性混成自動機,提出了基于路徑的有界可達性檢驗方法及相關(guān)優(yōu)化技術(shù)。通過將路徑可達性問題轉(zhuǎn)換成一組帶量詞的非線性約束的可滿足性問題,可以調(diào)用非線性約束求解器進行判定,在此基礎(chǔ)上使用深度優(yōu)先搜索依次枚舉并驗證閡值內(nèi)的候選路徑,從而完成有界可達性檢驗。進一步,提出了一種從非線性約束里抽取IIS的分析算法,可以從不可行的路徑里定位出不可行子路徑片段以約減狀態(tài)空間。受限于當(dāng)前底層支撐工具和非線性約束求解器的能力,所提方法目前僅得到可行性驗證,其有效性還有待進一步的驗證。
【學(xué)位授予單位】：南京大學(xué)
【學(xué)位級別】：博士
【學(xué)位授予年份】：2016
【分類號】：TP301.1

【相似文獻】

中國期刊全文數(shù)據(jù)庫 前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期

中國重要會議論文全文數(shù)據(jù)庫 前1條

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

中國博士學(xué)位論文全文數(shù)據(jù)庫 前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年

中國碩士學(xué)位論文全文數(shù)據(jù)庫 前6條

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

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

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

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

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

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

，

本文編號：1294546