利用随机模型检测技术来分析无线传感器网络的可生存性

　无线传感器网络是由部署在监控区域内的大量具有自治和无线通信协作能 力的传感器节点组成的一个多跳自组织网络。在大多数情况下网络不可能检测和 阻止所有的入侵，因此必须保证在发生入侵的情况下关键设施不间断的提供服 务。可生存性正式为此而诞生的关键服务保障技术。为了明确网络系统在遭遇故 障和攻击后究竟是否具有继续提供关键服务的能力，需要对可生存性进行评估， 以便于对可生存网络的设计与部署提供指导。

　　随机模型检测技术是一种对有限状态系统进行验证的技术，通过建立相应的 状态系统模型来描述待验证系统，使用逻辑公式形式化规约待验证的性质，然后 调用验证算法自动化完成性质的分析。随机模型检测高度自动化的特点在分析系 统可靠性，安全性等指标方面获得了广泛的认可和应用。

　　基于随机模型检测技术具有快速、可靠、易用等特点，本文将利用随机模型 检测技术来分析无线传感器网络的可生存性，主要工作有以下三个方面：

　　（1）建立了在发生故障和攻击下单节点行为演化的连续时间马尔科夫链模 型，通过单节点行为模型的组合方式建立了整个网络行为演化的连续时间马尔科 夫链模型。该网络模型能够刻画节点之间的连通关系，规避了现有基于模型的分 析技术对节点分布与拓扑结构的依赖性。

　　（2）PRISM 是目前最为先进的随机模型检测工具，使用 PRISM 需要使用者具 有一定的并发系统知识，而无线传感器网络领域的工作者相对比较缺乏，因此开 发了将网络的初始部署映射为一个 PRISM 建模语言描述的可生存评估模型的算 法，从而达到建模过程自动化的目的。

　　（3）为了量化网络系统在遭遇故障和攻击后继续提供关键服务的能力，建立了各种可生存性评估指标的连续随机逻辑 CSL 刻画，包括 k-connectivity 概率、 稳态可用性等等。将所建模型与描述可生存指标的 CSL 公式输入 PRISM，即可 完成可生存评估指标的自动化计算。这种应用逻辑描述评估指标的方式，可以使 只关注于指标本身，而不用关心得到指标数值的计算过程.