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

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

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

【相似文獻(xiàn)】

中國期刊全文數(shù)據(jù)庫 前10條

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

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

3 范雙南;;基于時(shí)間序列分析的混成系統(tǒ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 趙劍;歐陽丹彤;王曉宇;張立明;;混成系統(tǒng)的分布式診斷方法[J];吉林大學(xué)學(xué)報(bào)(工學(xué)版);2012年06期

8 肖娟;;混成系統(tǒng)的形式驗(yàn)證[J];長沙通信職業(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期

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

，

本文編號：1294546