无线传感器网络协议的随机时间自动机建模与评估方法

可在www.sciencedirect.com在线获取理论计算机科学电子笔记296（2013）261-277www.elsevier.com/locate/entcs无线传感器网络协议的随机时间自动机建模与评估Fengling Zhang，Lei Bu，Linzhang Wang，JianhuaZhao，Xin Chen，Tian Zhang，and Xuandong Li南京大学软件新技术国家重点实验室，江苏，中国电子邮件：zfl@seg.nju.edu.cn，bulei@nju.edu.cn摘要无线传感器网络广泛应用于各种环境中。它们可能会遇到大量的随机不确定性和干扰，如消息丢失和节点动态。 因此，以确保无线传感器网络底层协议的正确性，并评估其在不同环境下的性能。本文提出了一种基于随机时间自动机和统计模型检测的无线传感器网络协议分析与评估方法。对于建模，无线传感器网络协议的工作流程可以用经典的时间自动机建模。 然后，为了对现实环境中常见的消息丢失和节点动态等不确定性进行建模，可以通过随机变迁对时间自动机进行扩展，从而得到随机时间自动机。对于分析，协议的正确性可以回答经典的时间自动机上的模型检查，而在现实环境下的协议的性能可以评估的随机模型上的统计模型检查。 为了说明本文提出的建模和验证方法的可行性和可扩展性，本文给出了传感器网络定时同步协议（TPSN） 将在整个论文中进行全面研究关键词：无线传感器网络协议，建模与评估，随机时间自动机，统计模型检测1介绍无线传感器网络（Wireless Sensor Networks，WSNs）已经引起了世界范围内的广泛关注，并被广泛应用于军事行动、医疗保健、环境监测和保护等领域[1]。无线传感器网络中的所有高层应用都是基于其底层协议工作的。为了正确、高效地运行这些应用，底层无线传感器网络协议必须具有健壮性和可靠性。此外，无线传感器网络中的设备通常很难改变一旦部署，所以我们必须确保协议在设计阶段的目标环境下工作良好目前，对协议正确性的检验方法主要有仿真、测试和形式化验证。可以使用模拟和测试1571-0661 © 2013 Elsevier B. V.在CC BY-NC-ND许可下开放访问。http://dx.doi.org/10.1016/j.entcs.2013.09.001262F. Zhang等人/理论计算机科学电子笔记296（2013）261检查大规模网络并发现错误，但它们不能保证探索系统中所有可能的错误。因此，研究人员试图使用形式化建模和验证来对系统的行为进行建模，并证明所研究系统的正确性[2]。对于建模，由于WSN协议总是与实时行为紧密联系，时间自动机[5]是WSN系统的自然建模语言。像[16]，[17]，[18]这样的研究试图使用时间自动机来建模系统的工作但经典的时间自动机只能模拟理想情况下的系统行为。由于无线传感器网络系统可以部署在任何环境中，他们可能会遇到许多种不确定性，如消息丢失和节点动态。因此，在时间自动机中引入随机行为来支持对不确定性行为的建模，使模型更符合实际情况是非常重要的。对于验证，模型检查已被广泛用于检查WSN协议的正确性[15] [16] [19]。它可以探索协议模型的完整状态空间。然而，这种技术非常昂贵。它面临着臭名昭著的状态爆炸问题，并限制了可以检查的网络的规模。由于无线传感器网络通常由几十个节点组成，经典的模型检测方法不能很好地处理实际的无线传感器网络幸运的是，统计模型检查（SMC）最近被提出作为一种替代方案，以避免对模型状态空间的穷举探索[3]。SMC是一种基于模拟的解决方案，它比经典的模型检查时间和内存密集度更低[13]。SMC的过程是为系统生成足够多的样本执行路径，然后使用统计假设检验来决定系统是否满足给定的属性。SMC技术也可以用来估计系统满足给定属性的概率[3]。结合这些技术，本文提出了一种新的方法来建模和评估无线传感器网络协议的随机时间自动机和统计模型检测。首先，我们提出用时间自动机来描述无线传感器网络协议在理想环境下的工作流程对于无线传感器网络中常见的网络动态、节点故障和间歇性通信链路[1，6]，我们扩展了具有随机变迁的时间自动机。例如，在扩展的随机时间自动机中，当消息被广播时，它有概率丢失，而不是所有节点都成功接收到它。类似地，在真实环境中，节点可能随时死亡并离开网络，并且它可以复活并也随机重新加入网络。对于评估，我们建议协议设计的正确性可以通过对其理想模型进行模型检查来验证。例如，协议中是否存在死锁，协议是否能够成功实现其声称的功能等。此外，通过统计模型检验技术[8]，我们可以通过调整系统上的概率因子来检验协议在不同环境下的性能，比如当消息丢失概率在10%左右时，协议能够正确工作的概率是多少？为了说明上述方法，我们提出了一个完整的研究建模F. Zhang等人/理论计算机科学电子笔记296（2013）261263并对一种著名的无线传感器网络协议--传感器网络定时同步协议（TPSN）[4]进行了评价，认为TPSN具有精度高、适用于多跳网络的优点[4]。利用本文提出的建模和验证方法，我们可以发现，虽然该协议的设计总体上是正确的，但该协议对环境极其敏感，当系统被要求工作在恶劣环境中时，该协议并不适合作为候选协议。本文的结构如下。第二部分介绍了本研究的基本知识，包括无线传感器网络协议建模和验证的现有工作，并简要描述了随机时间自动机及其验证。在第三节中，我们提出了我们的方法来建模和评估一个协议的随机时间自动机。第四节给出了一个著名的无线传感器网络协议的随机时间自动机和相应的评估。第五部分是最后一部分的结束语.2背景2.1相关工作到目前为止，还没有统一的方法来建模和验证无线传感器网络协议。无线传感器网络协议的建模和验证的相关工作通常通过以下方式进行一个著名的WSN协议-泛洪时间同步协议（FTSP）在[14在[14]中，Kusy等人考虑了无线传感器网络系统中的复杂环境，并提出无线电消息将由于链路故障而以一定概率被丢弃。然而，由于状态空间爆炸，他们只检查FTSP在网络中有2个节点没有节点和链路故障。[15]验证了FTSP的几个重要性质，并表明网络可以收敛到单个根节点，并同意全局时间。但与[14]类似，他们在模型中没有考虑链路和节点故障。在[16]中，他们建模并验证了由2-7个节点组成的网络。在一个特定的场景中描述了一个错误，其中两个节点在整个工作同步后失败。由于状态空间爆炸，时钟漂移和链路故障没有被引入到他们的模型。在[17]和[18]中，Vaandrager等人也以类似的方式对WSN协议进行建模。他们用全连接拓扑验证了协议，并分析了模型检查器给出的反例。然而，他们的模型也没有包含系统的所有特征，例如不确定的通信延迟和不可靠的无线电通信。在[19]中，给出了时间同步传感器网络协议（TPSN）的时间自动机在这个时间自动机中，描述了TPSN在理想环境下的工作流程。验证所有节点是否都能与根节点同步，节点与根节点之间的时钟漂移是否有界等属性它们引入整数时钟来读取和分配本地时钟的值。然而，在这方面，1本文的部分思想发表在我们正在进行的抽象自然海报中[22]。264F. Zhang等人/理论计算机科学电子笔记296（2013）261该操作增加了模型的复杂性。他们验证的系统规模只有3-5个节点。此外，他们还有一些方法可以用其他语言对协议进行研究[20]给出了一种通过概率模型检查和PRISM [21]来检查移动WSNs性能的方法。他们建议用随机π演算来建模系统，并将其翻译成PRISM语言来检查这些属性。由于大多数无线传感器网络协议是时间相关的，π演算不能很好地支持这方面。此外，概率模型检查是非常昂贵的，这限制了可以分析的系统的大小综上所述，我们可以看到，首先，大多数建模和评估工作仍然将WSN协议视为通用协议。只有少数人考虑到模型的不确定性行为，这是非常普遍的无线传感器网络，到系统模型。第二，大多数的工作只检查了协议的正确性，只有少数的工作考虑了在不同的配置文件或环境下对协议性能的评估最后但并非最不重要的是，由于最常用的分析技术是非常昂贵的模型检查和/或概率模型检查，因此可以分析的系统的大小是有限的。由于部署的无线传感器网络系统规模往往很大，现有的分析技术的可扩展性不能很好地处理实际系统。2.2时间自动机的随机建模与验证时间自动机[9]被广泛用于实时系统的行为建模和分析时间自动机是一个有限状态机，它有一组时钟，以确保遵守严格的时间约束，例如执行时间，响应时间和通信延迟。约束的最简单形式是将时钟值与时间常数进行比较[5]。时间自动机只允许简单约束的布尔组合，即，对于时钟变量的集合C，时钟约束δ的集合Φ（C）被归纳地定义为通过δ：= x ≤ n|n ≤ x| ¬δ|其中x是C中的时钟，n是整数常数。这些时钟变量在系统启动时以零开始，然后以相同的速率同步增加。时钟变量也可以作为不变量附加到位置。一个位置只有在其所有不变量都为真时才能被输入和停留。假设a，b等代表动作的有限个字母表，时间自动机的形式定义[9] Γ是元组，其中• L是一组有限的位置（或节点）• l0∈L是初始位置• E∈L×Φ（C）×φ× 2C×L是边的集合，• I：L→Φ（C）将不变量分配给位置在时间自动机中，事件被建模为转换。时钟约束，即边缘上的保护用于限制自动机的转换。过渡可以F. Zhang等人/理论计算机科学电子笔记296（2013）261265仅当值满足边缘上标记的保护时才采用时间自动机理论可以用来证明实时系统的正确性[5]。一般来说，涉及两种类型的属性，活性和安全性。由于检查活性是计算昂贵的，验证时间系统的主要任务集中在检查安全属性，可以通过遍历时间自动机的状态空间使用可达性分析来检查[9]。证明了时间自动机的可达性验证是可判定的，但代价仍然很高。时间自动机可以通过加权概率分支来模拟随机变迁，从而得到随机时间自动机。最近，统计模型检验（SMC）[12]被提出来回答随机系统的数值性质。它基于Monte Carlo模拟反复模拟系统模型以生成足够的样本执行路径，然后依赖于统计算法，如假设检验[11]，以获得整个设计正确性的估计[8，10]。由于使用样本执行，验证结果设H0为性质公式φ成立的假设，H1为另一假设.可以使用两个参数α和β来限制错误概率，其中α是给定H0成立时H1的最大可接受概率，如果H1成立，则接受H0的概率应不大于β[8]。然后，使用Wald的序贯概率比检验[ 11 ]等技术统计假设的序贯概率比检验是在没有预定数量的观测值的情况下进行的。相反，在实验的任何阶段，它都会决定接受/拒绝假设，或者通过进行额外的观察来继续实验。当且仅当假设被接受或拒绝时，过程终止[11]。研究[13]已经进行了这样的技术来回答随机时间自动机的数值特性3基于随机时间自动机的无线传感器网络协议建模与评估在本节中，我们提出了一种方法来建模和评估无线传感器网络协议thor-oughtly：• 对于建模，首先，使用时间自动机在理想环境中对协议的工作流程进行建模然后，为了对无线传感器网络行为中的不确定性进行建模，对工作流时间自动机进行随机变迁扩展，得到随机时间自动机。• 在评价方面，经典的模型检验可以对小规模系统的理想工作流时间自动机进行统计模型检验可以对随机模型进行检验，以评估不同环境下具有实际规模的系统性能。266F. Zhang等人/理论计算机科学电子笔记296（2013）2613.1无线传感器网络协议3.1.1基于时间自动机的在大多数WSN协议中，节点/传感器可以承担某些功能角色，即，发送方和接收方，在协议的工作过程中。对于具有相同角色的所有节点，它们基本上共享类似的行为。因此，我们可以使用一个模板时间自动机来描述这些节点在理想环境中的工作流程然后，可以为每个节点分配一个唯一的编号作为其标识。不同的节点可以通过共享变量相互通信，并通过同步消息相互对于一个描述节点行为的模板时间自动机，我们提出了自底向上的模板模型。自下而上是指协议的生命周期可以分为不同的模块/阶段。每个特定模块/阶段的时间自动机片段可以独立构建。然后，它们最终可以组合在一起，这可以使建模任务变得更加容易和可控。3.1.2具有随机变迁的扩展时间自动机无线传感器网络通常工作在恶劣的环境中。因此，在实际应用中可能会遇到消息丢失、节点动态等不确定性为了解决这些问题，使模型更加逼真，我们建议扩展的时间自动机与随机转换。扩展分两步进行。首先，将概率因子添加到接收消息的转换中，以对消息丢失进行建模。然后通过引入概率分支来模拟节点可能失效和复活的场景考虑到消息的丢失，当消息被广播时，不是所有节点都成功接收消息，而是每个节点都有失败的概率才能收到这条信息也就是说，它的一些邻居可以成功地接收到这个数据包，而它们中的一些不能得到这个数据包。为了解决这个问题，在我们的模型中，我们在消息的接收者处添加概率因子，成功接收消息的概率被标记为SUC，丢失消息的概率被标记为FAIL。当系统触发SUC分支时，变量根据接收到的消息进行更新，时间自动机进入下一个状态。另一方面，当FAIL分支被触发时，自动机忽略该消息并返回到原始状态。作为一个例子，图。1.一、(a)显示消息的接收。由于无线传感器网络中的节点资源有限，且通常部署在恶劣的环境条件下，无线传感器网络具有高度的动态性，网络拓扑结构不断变化。也就是说，网络中的节点频繁地失效和恢复。为了对这种行为进行建模，我们引入了一个新的状态，失败，以表示节点已经死亡的情况，因此将忽略系统中的任何传入消息。从理论上讲，一个节点可以在任何时候失效，即在时间自动机中的任何状态。我们通过允许节点随机地从任何状态进入失败状态来模拟这种情况。如图1.一、(b)，处于常规状态的节点可以跳转以FAIL的概率进入失败状态，或以SUC的概率停留在此状态。处于失败状态的节点也可以恢复并再次加入网络F. Zhang等人/理论计算机科学电子笔记296（2013）261267≤5HFHiYH5HFHiYHG公司简介F68&8SGDWH（））$I/公司简介）DiOHG）$I/68&(a)（b）第（1）款Fig. 1. 无线传感器网络中的模型解扰到目前为止，我们可以得到理想和随机时间自动机的无线传感器网络协议。在此基础上，利用经典的时间自动机对协议设计的正确性进行了验证。该随机模型可以对协议在不同环境下的性能进行评估。3.2无线传感器网络协议3.2.1基于经典模型检验的通过经典的模型检测技术对理想时间自动机进行正确性在这个阶段，我们可以检查协议的功能属性，例如是否有死锁，是否所有节点最终都可以同步等。由于时间自动机的经典模型检验具有很高的复杂性，因此只能在小规模系统上进行验证。通过检查功能属性，我们可以看到其逻辑设计的正确性，并在早期发现错误3.2.2基于统计模型检验的性能评估与经典的模型检测相比，统计模型检测具有更低的成本和更好的可扩展性。利用统计模型检验，我们可以检验随机时间自动机的数值性质。例如，我们可以检查系统在有限时间内满足给定性质的概率，如：Pr[time bound]（<> expr）。通过收集链路和环境的真实概率因子并将其引入模型2，可以方便地评估候选协议在目标环境中的性能。此外，在设计或部署协议时，可能有许多关键参数，其值对整个系统的性能至关重要。统计模型检验允许我们检查和比较系统在不同候选值下满足一定要求的概率。因此，通过对随机模型的统计模型检验，我们也可以达到参数配置的目标。4TPSN的随机时间自动机为了说明我们提出的方法的可行性和可扩展性，在本节中，我们给出了建模和评估时间同步协议的细节2这些因素的实际值可以从网络轮廓中获得268F. Zhang等人/理论计算机科学电子笔记296（2013）261传感器网络定时同步协议（TPSN）。4.1TPSN建模传感器网络的时间同步协议（TPSN）[4]是一个用于无线传感器网络的全网络时间同步协议。TPSN的工作流程是：在网络中建立一个层次结构，以指定的节点为根节点，然后分配所有其他节点的级别。这称为级别发现阶段。然后，每个节点通过双向消息交换与其上级节点同步，最终所有节点与根节点同步。这是同步阶段。4.1.1时间自动机TPSN模型如前所述，在我们的方法中，时间自动机是以自底向上的方式构建的每个阶段的时间自动机的详细信息如下：级别发现阶段：级别发现阶段旨在在网络中建立层次结构，指定节点作为根节点，每个其他节点分配一个级别。这部分的时间自动机显示在图。二、（一）. 在我们模型，允许系统在短时间内离开等待状态（WaitTime≤6，在这个例子中）。当网络启动时，指定节点，即，根节点被分配级别0，并直接进入发现状态，而其他节点进入初始状态。根节点通过广播级别发现分组来开始级别发现阶段，并进入广播状态，这意味着它已经完成了该阶段的工作接收到级别发现分组的根节点的邻居如果处于初始状态则进入发现然后，处于发现状态的节点将向邻居广播其级别发现消息。此过程将继续，直到网络中的每个节点都被分配了一个级别并进入广播状态。同步阶段：当级别发现阶段结束时，即网络中的每个节点都被分配了一个级别（计数==N，N是网络的节点号），或者根节点已经在广播中停留了足够长的时间。 的时间（WaitTime==MAXTIME），根节点通过广播时间同步分组来开始同步阶段。由于根节点持有全局标准时间，它直接进入同步状态。 级别1中的节点接收时间同步包，等待一个随机时间（5≤WaitTime≤ 10），然后进入Transmit状态，这意味着它们可以开始与根交换消息node. 通过广播同步脉冲分组，节点进入已发送状态，等待来自处于同步状态的上层 节 点 的 应 答 。 在 接 收 到 确 认 消 息 Ack 时 ， 节 点 将 其 时 钟 调 整 到 根 节 点（drift[id]==0）。 所有这些消息都被广播，并且第2层中的节点在第1层中至少有一个邻居，因此它可以偷听这些消息交换。当一个节点接收到来自上层节点的同步脉冲时，它将返回一个随机时间（8≤WaitTime≤ 15），等待上层节点之间的消息交换结束。然后，它发起与上层节点的消息交换。这个过程在整个网络中进行，直到所有F. Zhang等人/理论计算机科学电子笔记296（2013）261269：DiWiQJ%URDGFDVW[001 pdf 1st-31files]P\/HYHO>iG@！= ²：DiW：DiW7iPH = 6P\OHYHO>iG@！= ²WiPHBV\QF”P\/HYHO>iG@ == 1WiPHBV\QF”8 =：DiW7iPH=15iG == 0P1/HYHO>iG@ =0，：DiW7iPH = 0，iG == 0iG！0：DiW7iPH =0&&01 - 02 - 025 =：DiW7iPH=10__ FRXQW == 1）5HFHiYH6\QFF7UDQVPiWDiVFRYHUHG爱奇艺WiDOFWiPHBV\QF！iG ==0&&/HYHOBGiVFRYHU\>j@”OHYHOBGiVFRYHU，：DiW7iPH = 0，：DiW7iPH == 5（61&：DiW7iPH stec = 7I0（2875H7UDQVPiW--5H7UDQVPiW！= 0[\fnSimHei\bord1\shad1\pos（200，288）}：DiW7iPH =0P\/HYHO>iG@ == P\/HYHO>j@+1FRXQW++OHYHOBGiVFRYHU\>iG@！：DiW7iPH = 0：DiW7iPH = 0，$FN>iG@！HGGUIW>IG@ = 07UDQVPiWHG$FN>j@”P\/HYHO>iG@ == P\/HYHO>j@2011年[001 pdf 1st-31files]%URDGFDVWF(a) 级别发现阶段（b）同步阶段图二. TPSN的时间自动机节点进入同步状态。由于传感器节点间存在时钟漂移，因此需要周期性地进行时钟同步，将节点间的时钟漂移限制在较小范围内。同步化阶段与同步化阶段几乎相同。根节点在保持同步状态一段固定时间后再次广播时间同步分组。处于同步状态的其他节点将等待一段时间，然后广播同步脉冲分组，以开始与根节点的消息交换，如果它们处于级别1的话。否则，它们将跳转到广播状态，等待来自上一级的同步脉冲。同步阶段的时间自动机如图所示。二、（b）.特殊规定：在我们的时间自动机中，我们还对作者在简介[4]中强调的特殊情况进行了首先，本地级发现是由网络的主要部分已经完成级发现阶段之后新节点加入系统引起的。如图3 .第三章。(a)，如果节点已处于初始状态一段时间，但尚未接收对于来自邻居节点的任何级别发现消息，其超时并广播级别请求消息以请求级别。邻居通过发送他们的级别来回复这个请求。如果有两个或更多的回复，它会给自己分配一个比最小的回复大一级的回复。由于节点加入网络的时间是不受限制的，只要节点被分配了级别，就可以随时回复级别请求包其次，传感器节点也可能随机死亡。如果节点不能得到应答，则它将在一段时间后发送同步脉冲。在重传固定次数的同步脉冲后，节点假设它已经失去了上层的所有邻居，并跳转到超时状态，然后它广播一个级别请求消息。在得到回复时，节点被分配一个新的级别，并再次加入分层结构。这部分时间自动机如图所示3 .第三章。（b）.到目前为止，我们可以将时间自动机的各个部分结合在一起，得到一个完整的模型来描述TPSN在理想环境下的整个工作流程，如图所示。四、270F. Zhang等人/理论计算机科学电子笔记296（2013）261：DiWiQJDiVFRYHUHG%URDGFDVWOHYHOBGiVFRYHU\>iG@！：DiWiG == 0V\QFKURQi]DWiRQBSXOVH>j@”P\/HYHO>iG@= 0P\/HYHO>iG@！²iG！0OHYHOBGiVFRYHU\（j）UHSO\>j@”QHZ/HYHO（j）爱奇艺WiDOFiG == 0P\/HYHO>iG@ == 1WiPHBV\QF”FiG == 0&&：DiW7iPH == 5（61&P\OHYHO>iG@！=²WiPHBV\QF”F：DiW7iPH！= 8F7UDQVPiWF5H7UDQVPiW！=0V\QFKURQi]DWiRQBSXOVH>iG@！FOHYHOBUHTXHVW>IG@！FWiPHBV\QF！：DiW7iPH stec = 7I0（287：DiW7iPH！= 55H7UDQVPiW7iPH2XW/HYHO5HTFP\OHYHO>iG@ == 1”WiPHBV\QF”GUiIW>iG@ = 0$FN>j@”F$FNQRZOHGJHPHQW[HG7UDQVPiWWHG$FN>iG@！：DiWiQJ爱奇艺WiDO7iPH2XWiG！0：DiW7iPH == 7iPH2XW：DiW7iPH：= 0FOHYHOBUHTXHVW>iG@！DiVFRYHUHGUHSO\>j”/HYHOBGiVFRYHU（j）UHSO\>j”QHZ/HYHO（j）/HYHO5HT%URDGFDVWOHYHOBUHTXHVW>j@”UHSO\>iG@！F7iPH2XW/HYHO5HTFOHYHOBUHTXHVW>IG@！[HG5H7UDQVPiW = 0P\/HYHO>iG@ == P\/HYHO>j@ +1：DiW7iPH = 0，GUiIW>iG@ = 0$FN>j@”5H7UDQVPiW！= 0F7UDQVPiW[\fnSimHei\bord1\shad1\pos（200，288）}：DiW7iPH = 0：DiW7iPH stec = 7I0（2875H7UDQVPiW：DiW7iPH = 07UDQVPiWHG(a)本地级发现阶段（b）级重新发现阶段图三. TPSN的时间自动机见图4。 TPSN的完全理想时间自动机4.1.2具有随机变迁在无线网络中，通信是不稳定的，消息广播时不可避免地会发生消息冲突因此，消息丢失是常见的。正如第3节中所提出的，我们使用随机转换来解决我们的时间自动机中的这种现象作为一个例子，图。五、(a)显示级别发现[id]的接收。为了模拟传感器网络中任何消息都可能丢失的现象，我们在模型中的每个消息接收转移中添加概率扩展类似地，为了对节点动态进行建模，我们引入了失败状态，表示节点已死亡，将忽略任何消息。我们允许自动机从任何状态随机进入失败状态。如图五、(b)处于常规状态的节点可以以FAIL的概率跳到Failed状态，或者以SUC的概率停留在该状态。处于失败状态的节点也可以恢复并再次加入网络。如果节点不是根节点，则它以概率SUC进入等待状态，并等待被分配新的级别。注意，当根节点被指定时，根节点的动态在模型中被简化。根节点可以从任何其他状态进入失败状态，类似于常规节点。但当它处于失败状态时，它会复活并直接进入等待状态，然后在整个网络中重新启动定时同步协议如图6、将上述方法集成到理想模型中，使无线传感器网络协议实时行为的不确定性可以在理想模型中得到描述。 由于篇幅所限，读者可参考http://seg.nju。edu.cn/people/www.example.com~bl/exp/TPSN.rar获取完整模型。F. Zhang等人/理论计算机科学电子笔记296（2013）261271%URDGFDVW：DiWiQJP\/HYHO>iG@ =DiVFRYHUHGiG == 00,：DiW7iPH =0，FRXQW++iG！0：DiW7iPH：=0：DiWOHYHOBGiVFRYHU\>iG@！FF爱奇艺WiDOF）DiOHGUHSO\>j”QHZ/HYHO（j）FFFF7UDQVPiWFFFFFOHYHOBUHTXHVW>iG@！F7iPH2XW/HYHO5HT FF$FN>iG@！$FNQRZOHGJHPHQW[HG7UDQVPiWHGIQiWiDO/HYHOBGiVFRYHU\>j@”j：1RGHVOHYHOBGiVFRYHU（j），WHPS =DiVFRYHUHGF68&FRXQW++，：DiW7iPH =0）$I/P\/HYHO>iG@ = WHPS）DiOHG68&）$I/爱奇艺WiDOiG！0）$I/iG == 068&：DiWiQJ（一）（b）第（1）款图五、具有概率的TPSN扩展时间自动机见图6。 TPSN的随机时间自动机4.2TPSN验证在4.1节中，我们分别给出了TPSN的理想时间自动机和随机时间自动机。在本节中，我们将基于这些模型分析TPSN我们验证了理想的时间自动机对典型的功能属性和评估TPSN的性能在不同的环境下使用统计模型检测技术的随机时间自动机。我们所验证的系统是一个具有N个节点的TPSN系统。 换句话说，它是一个由N个自动机组成的时间自动机网络。本文研究的TPSN系统的拓扑结构是全连通的。网络中的所有节点都是彼此的邻居3。我们使用的电脑配备英特尔®酷睿™ 2 QuadQ9500 处理器、2G内存及视窗7 专业版。我们使用的模型检查器是UPPAAL（V.4.1.7）[7]。在统计模型检查实验中使用的假阴性（α）和假阳性（β）都被设置为0.05。4.2.1TPSN正确性验证TPSN旨在实现全网同步。在协议概要中，该过程被指定为两个阶段，因此需要分别检查我们检查的属性如下：3通过修改拓扑矩阵可以很容易地改变被验证系统的拓扑结构在模型中读者可以参考完整的模型以了解详细信息。272F. Zhang等人/理论计算机科学电子笔记296（2013）261表1时间自动机N3456水平转让（C（T/M））Y（0.031/13）Y（0.032/19）Y（0.25/32）Y（3.791/17）节点同步（C（T/M））Y（0.031/14）Y（0.53/20）Y（43.384/31）Y（16984.546/47）有界时间范围（C（T/M））Y（0.031/15）Y（0.249/19）Y（10.28/47）Y（3024.326/430）无死锁Y（0.047/15）Y（0.375/18）Y（15.865/47）Y（3603.202/580）• Level Assignment：检查网络中的每个节点是否都可以分配一个级别。在这个模型中，节点因此，这个属性可以通过CTL公式指定为：A<>N（id：Nodes）myLevel [id] （id：Nodes）tpsn（id）. Synchronized。• Bounded Time Range：另一个判断TPSN是否能正常工作的属性是检查常规节点和根节点之间的时钟漂移是否在合理的范围内。此属性由以下人员检查：A []drift [id]<。• Deadlock Free：Last但至少， 没有 死锁：A []不是死锁。我们用UPPAAL在时间自动机中的3-6个处理器/节点的网络上检查这些性质。所有这些性能都得到了满足，这意味着TPSN可以在理想的环境中正常工作。验证结果（性能是否满足（C：是/否）、CPU时间（T：秒）和内存使用（M：MB））见表1。验证结果表明，TPSN的设计逻辑基本正确，如果所有的消息都没有任何错误地传输，并且节点一直工作良好，则4.2.2TPSN的性能测量在设计一个协议或选择在一个系统中使用哪种协议时，设计者/使用者除了要知道协议的功能是否正确外，还关心协议在特定目标环境下的性能。实际上，在TPSN中，有许多因素与系统的性能密切相关，• 恢复间隔：恢复间隔（RESYNC）是TPSN设计中的一个这个因素的大小对系统在选择RESYNC的值时有一个权衡。它应该足够长，以帮助同步在同步周期内完成;另一方面，它也必须尽可能短，以将两个节点之间的时钟漂移限制在小范围内[4]。因此，找到一种方法来更容易地为该因子选择合适的值• 同步时间：当TPSN工作良好时，人们关心的一个重要方面是协议的效率，例如同步所有 节点。为了分析效率，我们验证了所有节点的概率F. Zhang等人/理论计算机科学电子笔记296（2013）2612730.250.20.150.10.0550 90120 150200 300 500 1000 2000重新同步图第七章失效概率= 0.1的RESYNC数据在M个同步化阶段中成功同步，即， Pr[time<=M_N_C]（<> forall（i：Nodes）tpsn（i）.Synchronized）• 故障概率：故障概率是系统中消息丢失和/或节点动态的概率值。在我们的模型中，它的值由FAIL/（FAIL+SUC）决定。 用户想知道它如何影响TSPN的性能。例如，如果系统被假定为工作在恶劣的环境下，如果失效概率的影响很大，则该协议可能不是一个合适的选择。现在，我们开始通过统计模型检查在随机时间自动机中数值分析TPSN的性能，这些关键因素如下。恢复间隔：我们在时间自动机中对恢复进行了建模。为了说明RESYNC如何影响TPSN的性能，我们验证了一系列具有3-10个节点的网络，并记录了系统在不同RESYNC下在一个周期内同步的概率。验证结果如图所示7，失效概率为0.1。从图中可以看出，随着RESYNC的增加，在一个周期内同步所有节点的概率首先迅速增加;然后当RESYNC值接近150时，概率趋于稳定;一旦RESYNC大于150，概率仅略有波动。我们可以看到，即使RESYNC足够大，即2000，在最好的情况下，所有节点在第一个周期中同步的概率约为0.2。这是因为在极端情况下，节点可能会重复超时，从而无法在一个周期内与其他节点同步。因此，我们可以选择一个合适的RESYNC值，而不是增加RESYNC的值并等待所有节点同步，然后系统可以快速重新开始从这项研究来看，150个时间单位似乎是RESYNC的合适参考值。因此，在以下实验中，RESYNC将被设置为150。N=3N=4N=5N=6N=7 N=8N=9 N=10同步概率274F. Zhang等人/理论计算机科学电子笔记296（2013）261表2失效概率集为0的随机时间自动机在M个区间内的同步概率 和0.1失效概率= 0失效概率= 0.1NM=1M=2M=3M=1M=10M=100男=400人3[0.84，0.94][0.95，1][0.95，1][0.17，0.27][0.31，0.41][0.65，0.75][0.93，1]4[0.86，0.96][0.95，1][0.95，1][0.08，0.18][0.14，0.24][0.40，0.50][0.82，0.92]5[0.88，0.98][0.95，1][0.95，1][0.02，0.12][0.09，0.19][0.27，0.37][0.62，0.72]6[0.88，0.98][0.95，1][0.95，1][0.03，0.13][0.03，0.13][0.13，0.23][0.41，0.51]7[0.89，0.99][0.95，1][0.95，1]【0，0.10】[0.02，0.12][0.07，0.17][0.25，0.35]8[0.89，0.99][0.95，1][0.95，1]【0，0.07】【0，0.09】[0.01，0.11][0.15，0.25]9[0.87，0.97][0.95，1][0.95，1]【0，0.06】【0，0.07】【0，0.09】[0.06，0.16]10[0.88，0.98][0.95，1][0.95，1]【0，0.06】【0，0.07】【0，0.07】[0.02，0.12]20[0.85，0.95][0.95，1][0.95，1]【0，0.05】【0，0.05】【0，0.05】【0，0.05】同步时间：当TPSN工作正常，网络中的所有节点最终都可以同步时，我们感兴趣的是同步所有节点所花费的时间，以评估协议的效率在随机模型中，失效概率设为0和0.1时，所有节点在M个周期内同步的概率验证结果如表2所示。我们可以看到，当环境稳定时，随着网络中节点数量的增加，在某些时间段内成功同步的概率变小，这意味着需要更长的时间才能实现同步。此外，当环境恶化时，TPSN的性能急剧下降例如，当故障概率为0时，对于具有10个节点的系统，3个周期足以使所有节点同步。当失效概率为0.1时，对于同样的问题，即使是400次循环，所有节点同步的概率也只有[2%，12%]左右此外，即使网络中只有3个节点，也需要超过400个周期来确保网络同步。我们不断增加系统中的节点数，发现当节点数达到20时，使整个系统达到同步的概率稳定在5%以内。同样的故事发生在100个节点的系统上。这些现象意味着对于具有中等尺寸的TPSN系统，例如，TPSN节点数超过20个，在有轻微干扰的环境中几乎不可能正常工作。因此，我们在本研究中仅报告3-20个节点的数据。从这些数据中，我们惊讶地看到，TPSN的性能对环境是敏感的。 而且，节点数越多，故障概率引起的扰动越严重。因此，我们决定深入挖掘，看看环境如何才能真正影响TPSN。失败概率：在最后的实验中，我们发现消息丢失和节点动态可以大大影响TPSN的性能。 知道细节对于环境对TPSN的影响，例如环境变差时协议的性能会如何，进行了更多的实验。我们检查了由3个节点组成的系统在M个周期内成功同步的概率，故障概率分别为0，0.1，0.2和0.3结果绘制在Fig.八、F. Zhang等人/理论计算机科学电子笔记296（2013）26127510.90.80.70.60.50.40.30.20.1010 100 400 1000 5000同步周期见图8。具有不同失效概率（FP）的图中数据结果表明，随着失效概率的增加，TPSN的性能下降非常快。当失效概率为0时，即协议工作在理想环境下，我们几乎可以保证所有节点在10个同步周期内达到同步。当故障概率为0.1时，所有节点同步所需的时间更长。但是，仍然可以保证所有节点可以在400个周期内同步。同时，当失效概率为0.2时，即使在5000次循环中，失效概率也小于40%更不用说当故障概率为0.3时，在同一个系统中，几乎不可能在5000个周期内同步所有节点。从这些研究中我们可以看出，TPSN的性能是非常敏感的消息丢失和节点的动态，即使是一个小的无线传感器网络系统，只有3个节点，不能在恶劣的环境。5结论在本文中，我