论文部分内容阅读
无线网络通过多样的无线网络架构和动态频谱获取技术，给用户带来更多的便利。然而，由于复杂多变的电磁环境以及人们对无线应用的多样化需求，无线网络对开发人员提出了多种挑战。对于分布式的无线通信网络，自动化分析网络的所有可能行为是至关重要的。近年来，模型检测技术已经成为确保复杂协议正确性的一种重要方法。模型检测工具SPIN已经成功地应用于分析和建模众多协议，包括路由器协议、滑动窗口协议、X.509认证协议和WAP传输层协议。
本文首先介绍了形式化分析方法，然后分析了模型检测工具SPIN的原理，以及SPIN的建模语言PROMELA和线性时序逻辑公式LTL的基本理论。本文阐述了SPIN工具在认知无线电网络分布式协同感知协议验证中的应用。运用有限自动机FSA理论，构建协议的自动机模型和PROMELA验证模型，并采用多种方法减少验证模型的状态空间。此外，在线性时序逻辑LTL理论指导下，提出了该协议需要满足的正确性属性，发现了该协议在软件测试和SPIN的仿真运行过程中并未发现的脆弱性。