基于概率模型檢測的生存性分析與驗(yàn)證方法研究.pdf

1、模型檢測作為一種重要的形式化驗(yàn)證技術(shù),具有可靠、高效的優(yōu)點(diǎn),能夠?qū)崿F(xiàn)自動驗(yàn)證,獲得了越來越多的關(guān)注,并在硬件電路、通信協(xié)議、控制系統(tǒng)、安全認(rèn)證協(xié)議等方面的分析與驗(yàn)證中取得了巨大的成功。BDDs、符號化模型檢測等優(yōu)化技術(shù)的出現(xiàn),很大程度上緩解了狀態(tài)爆炸問題,使模型檢測工業(yè)化應(yīng)用成為可能。生存性作為軟硬件系統(tǒng)抵御災(zāi)難、自我修復(fù)能力的描述,成為網(wǎng)絡(luò)研究的一個(gè)熱點(diǎn)。生存性的準(zhǔn)確定義尚不明確,其定義及分析方法的研究是生存性研究的主要方向。論文將模

2、型檢測技術(shù)應(yīng)用于生存性分析,深入研究了形式化分析生存性的方法。完成的主要工作如下:
　　 1、闡述了模型檢測的框架和概率模型檢測的內(nèi)容,詳細(xì)介紹了基于DTMC、CTMC、PTA模型的三類不同的概率模型檢測方法,深入分析了這些概率模型檢測的特點(diǎn)、表述的能力和實(shí)現(xiàn)的難易程度。
　　 2、在生存性及概率模型檢測的基礎(chǔ)上,提出了驗(yàn)證生存性的模型檢測方法.首先給出適用于模型檢測的生存性定義,以及采用模型檢測驗(yàn)證生存性的方法:然后采

3、用PRISM,對電話接入網(wǎng)建模并驗(yàn)證其生存性。通過與數(shù)值計(jì)算的結(jié)果對比分析,證明了形式化方法分析生存性的正確性。
　　 3、針對考慮時(shí)延、能耗約束的隨機(jī)系統(tǒng)驗(yàn)證問題,提出了帶有補(bǔ)償約束的概率模型檢測方法。首先構(gòu)造帶補(bǔ)償約束的DTMC模型,并轉(zhuǎn)化成等價(jià)的權(quán)重圖.以滿足約束且概率最大為原則,將反例生成轉(zhuǎn)換成權(quán)重圖上多約束最短路徑問題;其次擴(kuò)展LTL-x邏輯,使其包含狀態(tài)公式與路徑補(bǔ)償公式,修改后的概率模型檢測具備了描述與驗(yàn)證補(bǔ)償約束