一种传感器网软件可达性验证方法
一种传感器网软件可达性验证方法
【专利摘要】本发明提出一种传感器网软件可达性验证方法，该方法首先将无线传感网软件用模型表示，该模型用来描述节点以及节点之间的状态迁移，然后用粒子群算法对所得的软件模型进行优化，在具体实施总可以时序逻辑公式来表示无线传感网软件所需要满足的属性或性质，将对无线传感网软件的验证转化为验证软件模型是否满足公式来判断系统性质。本发明方法通过对可达性验证路径的优化，能够有效地对传感器网软件进行可达性验证，并保持具有较强的灵活性。
【专利说明】一种传感器网软件可达性验证方法
【技术领域】
[0001]本发明涉及一种传感器网络软件可达性验证方法，主要利用模型检验技术来解决传感器网络软件验证问题，属于计算机科学与技术、软件工程和形式化验证、人工智能交叉技术应用领域。
【背景技术】
[0002]无线传感器网络是由部署在监测区域内的传感器节点通过无线通信方式形成的一个多跳自组织网络系统，目的是协作地感知、采集、处理和发布网络覆盖区域的对象信息。传感器节点是由传感器模块、处理器模块、无线通信模块和能量供应模块等部分组成，传感器模块负责监测区域的信息采集和数据转换；处理器模块负责控制传感器节点的操作，存储和处理采集到的数据以及其他节点发来的数据；无线通信模块负责与其他传感器节点进行无线通信，交换控制消息和收发采集数据；能量供应模块为传感器节点提供运行所需要的能量，通常使用微型电池。在无线传感器网络中，节点不是单个感知单元，而是能够交换信息、协调控制的有机结合体，整个网络实现物与物的互联，把感知触角深入世界各个角落，将成为下一代互联网的重要组成部分。
[0003]随着技术的不断发展，一方面无线传感器网络软件规模不断膨胀，软件系统变得越来越复杂，另一方面无线传感器网络应用对软件系统的可靠性提出了较高的要求。无线传感器网络软件系统不断膨胀的规模及其并发特性主要带来了内在非确定性，增大了验证系统可靠性的难度和代价。由于无线传感器网络现有程序开发语言本身具有不安全的特征，使利用传统方法来排除软件系统中的错误已经越来越难以满足实际需要。因此，如何保证软件正确性和可靠性成 为当前产业最紧迫的问题，在诸多问题解决方案中，模型检验等形式化验证技术在硬件和协议验证领域取得了成功，为应用于软件验证打下了基础。软件的形式化验证就是对无线传感器网络软件进行正确性证明。在软件形式化验证方法中，模型检验可以在构建系统前对系统的安全性和可靠性进行验证，以尽早发现错误，其基本原理是为系统建立形式化模型，阐述所要验证的性质，然后用算法去检测该模型是否满足所述性质。
[0004]模型检验的基本思想是用状态迁移系统(S)表示系统的行为，用模态/时序逻辑公式(F)描述系统的性质，这样“系统是否满足所期望的性质”就转化为数学问题“状态迁移系统S是否公式F的一个模型”，用公式表示为S I =F?。对有穷状态系统，这个问题是可判定的，即可以用计算机程序在有限时间内自动确定。模型检验提供一个完整的系统属性验证框架，其优点是模型检验能达到完全自动化的程度，只需用有穷状态模型和逻辑公式分别将系统实现和待验证的系统规范描述出来，之后的判断过程则完全可以由模型检验工具自动完成，不需要人的参与；模型检验过程总会以“是”或“否”的结果中止，当以“否”的结果中止时，说明设计或系统不满足某个给定的性质。此时一个违反性质的行为反例将会被给出，此反例将对理解错误的真正原因和修正错误提供线索。
[0005]粒子群算法最早是由Eberhart和Kelmedy于1995年提出的，它的基本概念源于对人工生命和鸟群捕食行为的研究。一群鸟在随机搜寻食物，在这个区域里只有一块食物，所有的鸟都不知道食物在哪里，但是它们知道当前的位置离食物还有多远。最简单有效的就是搜寻目前离食物最近的鸟的周围区域。
【发明内容】
[0006]技术问题:本发明的目的是提供一种传感器网软件可达性验证方法，用于解决传感网软件模型检验过程中出现的自动机模型冗余问题，本发明用粒子群优化算法优化自动机模型。
[0007]技术方案:本发明所述的传感器网软件可达性验证方法，首先将无线传感网软件用模型表示，该模型用来描述 节点以及节点之间的状态迁移，然后用粒子群算法对所得的软件模型进行优化，判读无线传感网软件状态之间的可达性。
[0008]本发明所述的传感器网软件可达性验证方法具体步骤如下:
[0009]步骤1、构建无线传感网软件模型，该模型用四元组(S，S0, R，L)形式来描述，其中S表不状态集合；Stl表不初始状态集合；R表不状态迁移,对任意一个a e R, a^=S><S,a (X0, X1)表示状态Xtl和状态X1之间存在状态迁移a，也可以表示为X1 = a (X0)jX0 e S，X1 e S山是用户指定的赋值函数，该函数用于对原子命题的赋值。
[0010]步骤2、给无线传感网软件模型中状态集合S的每一个状态赋予不同的序号，记录无线传感网软件每一个可能执行过程中的所有状态序列，每一个状态序列用执行过程中先后到达的状态的序号表不。
[0011]步骤3、用户标记目的状态Xn。
[0012]步骤4、依次选择步骤2中记录的无线传感网软件一个可能执行过程中的状态序列，查找该状态序列是否包含目的状态xn，若该状态序列包含目的状态xn，则删除该状态序列中状态Xn后的所有状态，进入步骤5 ;若该状态序列不包含目的状态Xn,进入步骤5。
[0013]步骤5、从状态X1开始，计算每个状态到目的状态的状态迁移量，所述状态迁移量是指状态到达目的状态的状态路径中包含的状态数目，设f⑴为第i个状态到目的状态的状态迁移量，pa，j)表示第i个状态的邻居状态j到目的状态的状态迁移量，Na)表示i状态的下一状态。
[0014]步骤6、计算任意一个状态Xi的f(i)和P(i，j)，判断f(i)与和P(i，j)的大小关系，若fa) ^ p(i, j)，则Xi与xnF连通，即状态不可达；若出现pa，j)〈fa)，则对于状态i，选定P(i，j)最小的Xj为状态Xi的下一跃迁状态，即N α) =χ」。
[0015]步骤7、判断Xj是否为目的状态Xn，若Xj = Xn,记录从X1到Xn的路径，循环结束，进入步骤8 ;若Xj古Xn,令i = j返回步骤6。
[0016]步骤8、使用一种模型检验工具建立传感网软件状态Xp X2.....Xn，用时序逻辑语
言表示用户指定的待验证的性质，根据用户标记目的状态Xn及步骤3到步骤7确定的从状态X1到状态Xn的路径，进行可达性验证，若存在到达目的状态的合法路径，则状态是可达的，反之状态不可达。所述模型检验工具是能够进行模型检验的系统验证软件。
[0017]有益效果:本发明所述的一种传感器网软件可达性验证方法，分析与应用相关的软件是否满足要求，分析能力强、可读性高，能尽早发现软件存在的缺陷和不正确性，其采用的形式化方法可以验证复杂系统。具体来说，本发明所述的方法具有如下的有益效果:[0018]1、本发明所述的传感器网软件可达性验证方法包括抽象模型生成、粒子群优化算法和模型检验。通过抽象化方法对传感器网络软件抽象化建模，利用粒子群优化算法分析优化，产生最优路径，最后利用模型检验技术进行传感网软件可达性验证。
[0019]2、本发明所述模型检验方法中的抽象模型生成模块实现将被检测的软件转换为一种形式化的状态自动机模型。
[0020]3、本发明所述的粒子群优化算法是将整个自动机看成一个粒子群，自动机的中的每个状态看成粒子，进而找出最优路径，具有较强的灵活性。
[0021]4、本发明所述粒子群优化算法将状态之间产生的最优路径记录下来，提高了传感网软件可达性验证效率。
【专利附图】
【附图说明】
[0022]图1是传感器网软件可达性验证具体实施流程图。
【具体实施方式】
[0023]本发明利用传感网协议ESAWN，该协议主要是处理传感网数据传输中多个节点向一个几点发送数据 的情况。节点数据通过传输路径分发和聚合到最后的根节点。为保证信息传输的正确性，协议设置监听者，假设节点nl将消息发送至n2，n2将消息发送至n3，依次进行，直到消息发送至根节点。我们将nl直接发送给n2，并设置监听者监听传送信息，当n3节点收到上一节点发送来的数据时，会自动与监听信息比较，判断信息是否正确。如图1，所示，结合传感网协议ESAWN，传感器网软件可达性验证方法具体实施步骤如下:
[0024]1、建立传感网协议ESAWN软件模型。所述模型用四元组(Sj^L)形式来描述，其中S表示状态集合Atl表示初始状态集合；R表示状态迁移，对任意一个a e R，a^SxS,a (X0, X1)表示状态Xtl和状态X1之间存在状态迁移a，也可以表示为X1 = a (X0)jX0 e S，X1 e S ;L是用户指定的赋值函数，该函数用于对原子命题的赋值。计算传感网协议ESAWN状态规模N，每一个状态的产生序号i，并记录所有可能的状态的执行序列，设定Si为状态序列中第i个状态。标记传感网协议ESAWN的目的状态Xn，简化执行序列，即所有的执行序列中若包含目的状态，则执行终止。
[0025]2、计算传感网协议ESAWN中每个状态到目的状态的状态迁移量，所述状态迁移量是指状态到达目的状态的状态路径中包含的状态数目。设f(i)为第i个状态到目的状态的状态迁移量，pa，j)表示第i个状态的邻居状态j到目的状态的状态迁移量，N α)表示
i状态的下一状态。然后计算传感网协议ESAWN中每个状态的f (i)和P (i，j)，判断自身状态迁移量与邻居状态迁移量大小关系。若f a) = P a，j)，则Xi与χη不连通，在具体实施中表示自动机不可达；若出现P (i，j) <f (i)，则对于状态i，选定P (i，j)最小的Xj为状态Xi的下一跃迁状态，即N (i) = Xj。判断Xj是否为目的状态Xn，若Xj = Xn,循环结束，若Xj Φ Xn,令i = j继续判断。
[0026]3、在具体实施中，使用UPPAAL、NuSMV等模型检验工具建立传感网软件状态X1'
X2.....Xn，用时序逻辑语言表示用户指定的待验证的性质，根据用户标记目的状态Xn及步
骤3到步骤7确定的从状态X1到状态Xn的路径，进行可达性验证，若存在到达目的状态的合法路径，则状态是可达的，反之状态不可达。
【权利要求】
1.一种传感网软件可达性验证方法，其特征在于该方法所包含的步骤为: 步骤1、构建无线传感网软件模型，该模型用四元组(SddL)形式来描述，其中S表示状态集合；S0表示初始状态集合；R表示状态迁移，对任意一个a e R’c^SxS, a (X0, X1)表示状态Xtl和状态X1之间存在状态迁移α，或表示为Xl = a (XO)，Xtl e S，X1 e S ;L是用户指定的赋值函数，该函数用于对原子命题的赋值； 步骤2、给无线传感网软件模型中状态集合S的每一个状态赋予不同的序号，记录无线传感网软件每一个可能执行过程中的所有状态序列，每一个状态序列用执行过程中先后到达的状态的序号表示； 步骤3、用户标记目的状态Xn; 步骤4、依次选择步骤2中记录的无线传感网软件一个可能执行过程中的状态序列，查找该状态序列是否包含目的状态Xn，若该状态序列包含目的状态Xn，则删除该状态序列中状态Xn后的所有状态，进入步骤5 ;若该状态序列不包含目的状态Xn,进入步骤5 ； 步骤5、从状态X1开始，计算每个状态到目的状态的状态迁移量，所述状态迁移量是指状态到达目的状态的状态路径中包含的状态数目，设f⑴为第i个状态到目的状态的状态迁移量，P(i，j)表示第i个状态的邻居状态j到目的状态的状态迁移量，N(i)表示i状态的下一状态； 步骤6、计算任意一个状态Xi的f(i)和P(i，j)，判断f(i)与和P(i，j)的大小关系，若f(i) ^ P(i, j)，则Xi与Xn不连通，即状态不可达；若出现P(i，j)<f(i)，则对于状态i，选定P(i，j)最小的为状态Xi的下一跃迁状态，即N(i) = Xj ； 步骤7、判断Xj是否为目的状态Xn，若Xj = Xn,记录从X1到Xn的路径，循环结束，进入步骤8 ;若Xj古Xn，令i = j返回步骤6 ； 步骤8、使用一种模型检验工具建立传感网软件状态Xp X2.....Xn，用时序逻辑语言表示用户指定的待验证的性质，根据用户标记目的状态Xn及步骤3到步骤7确定的从状态X1到状态Xn的路径，进行可达性验证，若存在到达目的状态的合法路径，则状态是可达的，反之状态不可达，所述模型检验工具是能够进行模型检验的系统验证软件。
【文档编号】G06F11/36GK103970653SQ201410179197
【公开日】2014年8月6日 申请日期:2014年4月29日 优先权日:2014年4月29日
【发明者】陈志 , 岳书珍, 岳文静, 王东, 陈骏, 党凯乐, 朱彦沛, 高阳阳, 高显强 申请人:南京邮电大学
【专利摘要】本发明提出一种传感器网软件可达性验证方法，该方法首先将无线传感网软件用模型表示，该模型用来描述节点以及节点之间的状态迁移，然后用粒子群算法对所得的软件模型进行优化，在具体实施总可以时序逻辑公式来表示无线传感网软件所需要满足的属性或性质，将对无线传感网软件的验证转化为验证软件模型是否满足公式来判断系统性质。本发明方法通过对可达性验证路径的优化，能够有效地对传感器网软件进行可达性验证，并保持具有较强的灵活性。
【专利说明】一种传感器网软件可达性验证方法
【技术领域】
[0001]本发明涉及一种传感器网络软件可达性验证方法，主要利用模型检验技术来解决传感器网络软件验证问题，属于计算机科学与技术、软件工程和形式化验证、人工智能交叉技术应用领域。
【背景技术】
[0002]无线传感器网络是由部署在监测区域内的传感器节点通过无线通信方式形成的一个多跳自组织网络系统，目的是协作地感知、采集、处理和发布网络覆盖区域的对象信息。传感器节点是由传感器模块、处理器模块、无线通信模块和能量供应模块等部分组成，传感器模块负责监测区域的信息采集和数据转换；处理器模块负责控制传感器节点的操作，存储和处理采集到的数据以及其他节点发来的数据；无线通信模块负责与其他传感器节点进行无线通信，交换控制消息和收发采集数据；能量供应模块为传感器节点提供运行所需要的能量，通常使用微型电池。在无线传感器网络中，节点不是单个感知单元，而是能够交换信息、协调控制的有机结合体，整个网络实现物与物的互联，把感知触角深入世界各个角落，将成为下一代互联网的重要组成部分。
[0003]随着技术的不断发展，一方面无线传感器网络软件规模不断膨胀，软件系统变得越来越复杂，另一方面无线传感器网络应用对软件系统的可靠性提出了较高的要求。无线传感器网络软件系统不断膨胀的规模及其并发特性主要带来了内在非确定性，增大了验证系统可靠性的难度和代价。由于无线传感器网络现有程序开发语言本身具有不安全的特征，使利用传统方法来排除软件系统中的错误已经越来越难以满足实际需要。因此，如何保证软件正确性和可靠性成 为当前产业最紧迫的问题，在诸多问题解决方案中，模型检验等形式化验证技术在硬件和协议验证领域取得了成功，为应用于软件验证打下了基础。软件的形式化验证就是对无线传感器网络软件进行正确性证明。在软件形式化验证方法中，模型检验可以在构建系统前对系统的安全性和可靠性进行验证，以尽早发现错误，其基本原理是为系统建立形式化模型，阐述所要验证的性质，然后用算法去检测该模型是否满足所述性质。
[0004]模型检验的基本思想是用状态迁移系统(S)表示系统的行为，用模态/时序逻辑公式(F)描述系统的性质，这样“系统是否满足所期望的性质”就转化为数学问题“状态迁移系统S是否公式F的一个模型”，用公式表示为S I =F?。对有穷状态系统，这个问题是可判定的，即可以用计算机程序在有限时间内自动确定。模型检验提供一个完整的系统属性验证框架，其优点是模型检验能达到完全自动化的程度，只需用有穷状态模型和逻辑公式分别将系统实现和待验证的系统规范描述出来，之后的判断过程则完全可以由模型检验工具自动完成，不需要人的参与；模型检验过程总会以“是”或“否”的结果中止，当以“否”的结果中止时，说明设计或系统不满足某个给定的性质。此时一个违反性质的行为反例将会被给出，此反例将对理解错误的真正原因和修正错误提供线索。
[0005]粒子群算法最早是由Eberhart和Kelmedy于1995年提出的，它的基本概念源于对人工生命和鸟群捕食行为的研究。一群鸟在随机搜寻食物，在这个区域里只有一块食物，所有的鸟都不知道食物在哪里，但是它们知道当前的位置离食物还有多远。最简单有效的就是搜寻目前离食物最近的鸟的周围区域。
【发明内容】
[0006]技术问题:本发明的目的是提供一种传感器网软件可达性验证方法，用于解决传感网软件模型检验过程中出现的自动机模型冗余问题，本发明用粒子群优化算法优化自动机模型。
[0007]技术方案:本发明所述的传感器网软件可达性验证方法，首先将无线传感网软件用模型表示，该模型用来描述 节点以及节点之间的状态迁移，然后用粒子群算法对所得的软件模型进行优化，判读无线传感网软件状态之间的可达性。
[0008]本发明所述的传感器网软件可达性验证方法具体步骤如下:
[0009]步骤1、构建无线传感网软件模型，该模型用四元组(S，S0, R，L)形式来描述，其中S表不状态集合；Stl表不初始状态集合；R表不状态迁移,对任意一个a e R, a^=S><S,a (X0, X1)表示状态Xtl和状态X1之间存在状态迁移a，也可以表示为X1 = a (X0)jX0 e S，X1 e S山是用户指定的赋值函数，该函数用于对原子命题的赋值。
[0010]步骤2、给无线传感网软件模型中状态集合S的每一个状态赋予不同的序号，记录无线传感网软件每一个可能执行过程中的所有状态序列，每一个状态序列用执行过程中先后到达的状态的序号表不。
[0011]步骤3、用户标记目的状态Xn。
[0012]步骤4、依次选择步骤2中记录的无线传感网软件一个可能执行过程中的状态序列，查找该状态序列是否包含目的状态xn，若该状态序列包含目的状态xn，则删除该状态序列中状态Xn后的所有状态，进入步骤5 ;若该状态序列不包含目的状态Xn,进入步骤5。
[0013]步骤5、从状态X1开始，计算每个状态到目的状态的状态迁移量，所述状态迁移量是指状态到达目的状态的状态路径中包含的状态数目，设f⑴为第i个状态到目的状态的状态迁移量，pa，j)表示第i个状态的邻居状态j到目的状态的状态迁移量，Na)表示i状态的下一状态。
[0014]步骤6、计算任意一个状态Xi的f(i)和P(i，j)，判断f(i)与和P(i，j)的大小关系，若fa) ^ p(i, j)，则Xi与xnF连通，即状态不可达；若出现pa，j)〈fa)，则对于状态i，选定P(i，j)最小的Xj为状态Xi的下一跃迁状态，即N α) =χ」。
[0015]步骤7、判断Xj是否为目的状态Xn，若Xj = Xn,记录从X1到Xn的路径，循环结束，进入步骤8 ;若Xj古Xn,令i = j返回步骤6。
[0016]步骤8、使用一种模型检验工具建立传感网软件状态Xp X2.....Xn，用时序逻辑语
言表示用户指定的待验证的性质，根据用户标记目的状态Xn及步骤3到步骤7确定的从状态X1到状态Xn的路径，进行可达性验证，若存在到达目的状态的合法路径，则状态是可达的，反之状态不可达。所述模型检验工具是能够进行模型检验的系统验证软件。
[0017]有益效果:本发明所述的一种传感器网软件可达性验证方法，分析与应用相关的软件是否满足要求，分析能力强、可读性高，能尽早发现软件存在的缺陷和不正确性，其采用的形式化方法可以验证复杂系统。具体来说，本发明所述的方法具有如下的有益效果:[0018]1、本发明所述的传感器网软件可达性验证方法包括抽象模型生成、粒子群优化算法和模型检验。通过抽象化方法对传感器网络软件抽象化建模，利用粒子群优化算法分析优化，产生最优路径，最后利用模型检验技术进行传感网软件可达性验证。
[0019]2、本发明所述模型检验方法中的抽象模型生成模块实现将被检测的软件转换为一种形式化的状态自动机模型。
[0020]3、本发明所述的粒子群优化算法是将整个自动机看成一个粒子群，自动机的中的每个状态看成粒子，进而找出最优路径，具有较强的灵活性。
[0021]4、本发明所述粒子群优化算法将状态之间产生的最优路径记录下来，提高了传感网软件可达性验证效率。
【专利附图】
【附图说明】
[0022]图1是传感器网软件可达性验证具体实施流程图。
【具体实施方式】
[0023]本发明利用传感网协议ESAWN，该协议主要是处理传感网数据传输中多个节点向一个几点发送数据 的情况。节点数据通过传输路径分发和聚合到最后的根节点。为保证信息传输的正确性，协议设置监听者，假设节点nl将消息发送至n2，n2将消息发送至n3，依次进行，直到消息发送至根节点。我们将nl直接发送给n2，并设置监听者监听传送信息，当n3节点收到上一节点发送来的数据时，会自动与监听信息比较，判断信息是否正确。如图1，所示，结合传感网协议ESAWN，传感器网软件可达性验证方法具体实施步骤如下:
[0024]1、建立传感网协议ESAWN软件模型。所述模型用四元组(Sj^L)形式来描述，其中S表示状态集合Atl表示初始状态集合；R表示状态迁移，对任意一个a e R，a^SxS,a (X0, X1)表示状态Xtl和状态X1之间存在状态迁移a，也可以表示为X1 = a (X0)jX0 e S，X1 e S ;L是用户指定的赋值函数，该函数用于对原子命题的赋值。计算传感网协议ESAWN状态规模N，每一个状态的产生序号i，并记录所有可能的状态的执行序列，设定Si为状态序列中第i个状态。标记传感网协议ESAWN的目的状态Xn，简化执行序列，即所有的执行序列中若包含目的状态，则执行终止。
[0025]2、计算传感网协议ESAWN中每个状态到目的状态的状态迁移量，所述状态迁移量是指状态到达目的状态的状态路径中包含的状态数目。设f(i)为第i个状态到目的状态的状态迁移量，pa，j)表示第i个状态的邻居状态j到目的状态的状态迁移量，N α)表示
i状态的下一状态。然后计算传感网协议ESAWN中每个状态的f (i)和P (i，j)，判断自身状态迁移量与邻居状态迁移量大小关系。若f a) = P a，j)，则Xi与χη不连通，在具体实施中表示自动机不可达；若出现P (i，j) <f (i)，则对于状态i，选定P (i，j)最小的Xj为状态Xi的下一跃迁状态，即N (i) = Xj。判断Xj是否为目的状态Xn，若Xj = Xn,循环结束，若Xj Φ Xn,令i = j继续判断。
[0026]3、在具体实施中，使用UPPAAL、NuSMV等模型检验工具建立传感网软件状态X1'
X2.....Xn，用时序逻辑语言表示用户指定的待验证的性质，根据用户标记目的状态Xn及步
骤3到步骤7确定的从状态X1到状态Xn的路径，进行可达性验证，若存在到达目的状态的合法路径，则状态是可达的，反之状态不可达。
【权利要求】
1.一种传感网软件可达性验证方法，其特征在于该方法所包含的步骤为: 步骤1、构建无线传感网软件模型，该模型用四元组(SddL)形式来描述，其中S表示状态集合；S0表示初始状态集合；R表示状态迁移，对任意一个a e R’c^SxS, a (X0, X1)表示状态Xtl和状态X1之间存在状态迁移α，或表示为Xl = a (XO)，Xtl e S，X1 e S ;L是用户指定的赋值函数，该函数用于对原子命题的赋值； 步骤2、给无线传感网软件模型中状态集合S的每一个状态赋予不同的序号，记录无线传感网软件每一个可能执行过程中的所有状态序列，每一个状态序列用执行过程中先后到达的状态的序号表示； 步骤3、用户标记目的状态Xn; 步骤4、依次选择步骤2中记录的无线传感网软件一个可能执行过程中的状态序列，查找该状态序列是否包含目的状态Xn，若该状态序列包含目的状态Xn，则删除该状态序列中状态Xn后的所有状态，进入步骤5 ;若该状态序列不包含目的状态Xn,进入步骤5 ； 步骤5、从状态X1开始，计算每个状态到目的状态的状态迁移量，所述状态迁移量是指状态到达目的状态的状态路径中包含的状态数目，设f⑴为第i个状态到目的状态的状态迁移量，P(i，j)表示第i个状态的邻居状态j到目的状态的状态迁移量，N(i)表示i状态的下一状态； 步骤6、计算任意一个状态Xi的f(i)和P(i，j)，判断f(i)与和P(i，j)的大小关系，若f(i) ^ P(i, j)，则Xi与Xn不连通，即状态不可达；若出现P(i，j)<f(i)，则对于状态i，选定P(i，j)最小的为状态Xi的下一跃迁状态，即N(i) = Xj ； 步骤7、判断Xj是否为目的状态Xn，若Xj = Xn,记录从X1到Xn的路径，循环结束，进入步骤8 ;若Xj古Xn，令i = j返回步骤6 ； 步骤8、使用一种模型检验工具建立传感网软件状态Xp X2.....Xn，用时序逻辑语言表示用户指定的待验证的性质，根据用户标记目的状态Xn及步骤3到步骤7确定的从状态X1到状态Xn的路径，进行可达性验证，若存在到达目的状态的合法路径，则状态是可达的，反之状态不可达，所述模型检验工具是能够进行模型检验的系统验证软件。
【文档编号】G06F11/36GK103970653SQ201410179197
【公开日】2014年8月6日 申请日期:2014年4月29日 优先权日:2014年4月29日
【发明者】陈志 , 岳书珍, 岳文静, 王东, 陈骏, 党凯乐, 朱彦沛, 高阳阳, 高显强 申请人:南京邮电大学
最新回复(0)