论文部分内容阅读
随着无线传感网络技术的发展，其应用范围日趋广泛。而协议作为无线传感网络通信的基础，其重要性显而易见，但由于无线传感网络运行环境的复杂性，协议的正确性很难得到保证。通常的协议分析方法，如仿真、测试虽然能够分析大规模网络，但不能验证协议的所有行为，从而可能漏掉一些极端错误场景，这对于环境复杂的无线传感网络的分析是不足够的。模型检验是一种形式化自动验证技术，其优势在于能够更加完备的探索系统行为，发现难以发现的错误，提高软件的可靠性。 时间同步作为网络提供的基本中间件服务，也是许多无线传感网络应用的基础。TheFlooding Time Synchronization protocol(FTSP)是为WSNs提出的一个对网络失效具备健壮性的洪泛式时间同步协议，其目的是达到网络范围的时间同步。该协议在实验室进行的仿真和测试分析中未发现错误，但在实际应用中却出现某些节点会突然与其它节点失去同步的情况。这些不稳定性被认为是由消息丢失和节点失效引起的。 本文使用模型检验的方法对FTSP对节点失效的健壮性进行了分析。其主要工作包括以下三点: 1)使用时间自动机对FTSP进行了建模。在建模过程中，我们主要描述FTSP的动态根节点选举算法，并分两个场景对其进行了分析:无节点失效场景和节点失效场景。我们还将传输时延引入了模型之中，使之更贴近WSNs实际运行情况。 2)基于不相关公式检测和偏序约简两种时间自动机可达性优化算法开发完善了具有图形建模界面的时间自动机可达性分析工具TAC，为以后的WSNs协议的验证提供了基础。 3)使用CTL对FTSP的健壮性进行了规约，并使用UPPAAL和TAC分别对FTSP的性质进行了验证。在验证过程中，我们发现当先后两个根节点连续失效时，FTSP根节点选举算法会进入死循环状态。