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

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

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

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

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

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