無線傳感器網絡是由部署在監控區域內的大量具有自治和無線通信協作能 力的傳感器節點組成的一個多跳自組織網絡。在大多數情況下網絡不可能檢測和 阻止所有的入侵，因此必須保證在發生入侵的情況下關鍵設施不間斷的提供服 務?？缮嫘哉綖榇硕Q生的關鍵服務保障技術。為了明確網絡系統在遭遇故 障和攻擊后究竟是否具有繼續提供關鍵服務的能力，需要對可生存性進行評估， 以便于對可生存網絡的設計與部署提供指導。

　　隨機模型檢測技術是一種對有限狀態系統進行驗證的技術，通過建立相應的 狀態系統模型來描述待驗證系統，使用邏輯公式形式化規約待驗證的性質，然后 調用驗證算法自動化完成性質的分析。隨機模型檢測高度自動化的特點在分析系 統可靠性，安全性等指標方面獲得了廣泛的認可和應用。

　　基于隨機模型檢測技術具有快速、可靠、易用等特點，本文將利用隨機模型 檢測技術來分析無線傳感器網絡的可生存性，主要工作有以下三個方面：

　?。?）建立了在發生故障和攻擊下單節點行為演化的連續時間馬爾科夫鏈模 型，通過單節點行為模型的組合方式建立了整個網絡行為演化的連續時間馬爾科 夫鏈模型。該網絡模型能夠刻畫節點之間的連通關系，規避了現有基于模型的分 析技術對節點分布與拓撲結構的依賴性。

　?。?）PRISM 是目前最為先進的隨機模型檢測工具，使用 PRISM 需要使用者具 有一定的并發系統知識，而無線傳感器網絡領域的工作者相對比較缺乏，因此開 發了將網絡的初始部署映射為一個 PRISM 建模語言描述的可生存評估模型的算 法，從而達到建模過程自動化的目的。

　?。?）為了量化網絡系統在遭遇故障和攻擊后繼續提供關鍵服務的能力，建立了各種可生存性評估指標的連續隨機邏輯 CSL 刻畫，包括 k-connectivity 概率、 穩態可用性等等。將所建模型與描述可生存指標的 CSL 公式輸入 PRISM，即可 完成可生存評估指標的自動化計算。這種應用邏輯描述評估指標的方式，可以使 只關注于指標本身，而不用關心得到指標數值的計算過程.