面向過去算子的隨機模型檢測算法與應(yīng)用.pdf

1、隨機模型檢測是一種將自動化與形式化相結(jié)合的系統(tǒng)驗證技術(shù)，其具有可靠、高效的優(yōu)點，并且能夠?qū)崿F(xiàn)自動化驗證，因此獲得了越來越多的關(guān)注，在硬件電路、控制系統(tǒng)、通信協(xié)議、安全認(rèn)證協(xié)議等方面的分析與驗證中已經(jīng)取得了巨大的成功。隨機模型檢測的主要思想如下，首先將目標(biāo)系統(tǒng)抽象成一個概率模型，并用概率時序邏輯刻畫需要驗證的屬性，然后判定模型是否滿足這些屬性，或是求解屬性的值。其中用來刻畫屬性的概率計算樹時序邏輯和連續(xù)隨機邏輯只能夠表達未來的運行狀況，然

2、而未來的運行狀況大多依賴于系統(tǒng)之前的行為，這兩種概率時序邏輯無法表達此約束，本文將分別在概率計算樹時序邏輯和連續(xù)隨機邏輯中引入過去算子，并給出了語義，語法以及相應(yīng)的模型檢測算法，使其能夠更全面的描述系統(tǒng)屬性行為。
　　無線傳感器網(wǎng)絡(luò)(WSNs)由于其高機動性，靈活性和無線特性，使其應(yīng)用范圍廣泛，其中包括健康檢測、軍事等關(guān)鍵領(lǐng)域，可生存性是WSNs研究的一個關(guān)鍵屬性，即評估網(wǎng)絡(luò)在存在異常事件，比如發(fā)生故障的情況下完成其任務(wù)的能力，本

3、文利用隨機模型檢測的方法對無線傳感器網(wǎng)絡(luò)的可生存性即網(wǎng)絡(luò)系統(tǒng)抵御災(zāi)難、自我修復(fù)的能力進行了詳細(xì)的分析，以上分析建模刻畫屬性并且進行驗證的工作均是在模型檢測工具PRISM上面完成的，本文的主要工作如下:
　　1.在概率計算樹邏輯和連續(xù)隨機邏輯中引入過去算子，增加規(guī)約語言的表達力。概率計算樹邏輯(PCTL)和連續(xù)隨機邏輯(CSL)主要刻畫了隨機系統(tǒng)未來的運行狀況，然而未來的運行狀況大多依賴于系統(tǒng)之前的行為，PCTL和CSL無法表達此約

4、束。為此在PCTL和CSL中分別引入過去時態(tài)算子，得到了表達力更強的屬性規(guī)約語言PPCTL和PCSL，進一步分別給出了PPCTL和PCSL的語義，語法及模型檢測算法。PPCTL的模型檢測算法的時間復(fù)雜性和PCTL的時間復(fù)雜性相同，即不會隨表達力的增加而增加，PCSL的模型檢測算法的時間復(fù)雜性和CSL的時間復(fù)雜性相同，也不會隨表達力的增加而增加。
　　2.應(yīng)用隨機模型檢測方法對無線傳感器網(wǎng)絡(luò)的可生存性進行分析評估。根據(jù)無線傳感器網(wǎng)絡(luò)

5、的網(wǎng)絡(luò)環(huán)境，利用連續(xù)時間馬爾科夫鏈(CTMC)建立系統(tǒng)模型，在建模的時候考慮了網(wǎng)絡(luò)環(huán)境中最常見的以下四種故障事件即節(jié)點故障，鏈接故障，節(jié)點身份偽造故障和損壞攻擊故障，其中損壞攻擊故障是由黑洞攻擊造成的，節(jié)點身份偽造故障是由女巫攻擊造成的，并且這兩種故障是相結(jié)合的，節(jié)點受到女巫攻擊，身份被偽造，該區(qū)域的路由就由該惡意節(jié)點獨自完成，再結(jié)合黑洞攻擊來破壞網(wǎng)絡(luò)的服務(wù);當(dāng)發(fā)生鏈接故障的時候，先找是否有替換鏈接，如果沒有再對鏈接進行修復(fù);模型建立以