面向過去算子的隨機模型檢測算法與應用.pdf

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

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

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

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

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