基于动态规划的传感器网络软件模型检验方法

摘要

本发明是一种基于动态规划的无线传感器网络软件模型检验方法，包括系统建模、模型预处理、模型性质验证等步骤。系统建模通过一套流程方法，建立抽象的时间状态自动机模型；模型预处理用于减少自动机中的对验证过程不产生影响的状态；模型性质验证采用基于动态规划思想的记忆化搜索验证方法。本发明能够有效地验证相关网络协议是否满足要求，缓解验证过程中状态空间爆炸问题，给出的系统验证过程时空复杂度低。

说明书

技术领域

本发明涉及一种在传感器网络软件模型检验中状态空间搜索的方法，主要利用动态规划思想来缓解状态空间爆炸问题，属于计算机技术、无线通信、传感器技术、拓扑控制技术和验证技术交叉技术应用领域。

背景技术

传感器技术、微机电系统、现代网络和无线通信等技术的进步，推动了现代无线传感器网络的产生和发展。无线传感器网络扩展了人们信息获取能力，将客观世界的物理信息同传输网络连接在一起，在下一代网络中将为人们提供最直接、最有效、最真实的信息。无线传感器网络是由一组传感器节点以自组织方式构成的无线网络，其目的是协作地感知、采集和处理网络覆盖地理区域中感知对象的信息，并发布给观察者。从上述定义可以看到，传感器节点、感知对象和观察者是无线传感器网络的3个基本要素。无线传感器网络可以被广泛地应用于军事应用、医疗护理、环境监测、空间探索、医疗卫生、制造业和反恐抗灾等领域。

模型检验方法可以在构建系统前对系统的安全性和可靠性进行验证，以尽早发现错误。模型检验是对有穷状态系统的一种形式化确认方法。它最早由Clarke和Emerson以及Quiele和Sifakis在1981年分别提出的，主要通过显式状态搜索或隐式不动点计算来验证有穷状态并发系统的模态/命题性质。实质是利用计算机的快速计算能力，通过穷举被检验系统的状态空间中的每一个状态来验证该系统满足特定的形式描述（模型检验过程图见附图1）。尽管限制在有穷系统上是一个缺点，但模型检验可以应用于许多非常重要的系统，如通信协议和电路的验证上。很多情况下，可以把模型检验和各种抽象与归纳原则结合起来验证非有穷状态系统（如实时系统），模型检验的基本思想是用状态迁移系统(S)表示系统的行为，用模态/时序逻辑公式(F)描述系统的性质，这样“系统是否满足所期望的性质”就转化为数学问题“状态迁移系统S是否公式F的一个模型”，用公式表示为S|=F？。对有穷状态系统，这个问题是可判定的，即可以用计算机程序在有限时间内自动确定。模型检验已被应用于计算机硬件、通信协议、控制系统、安全认证协议等方面的分析与验证中，取得了令人瞩目的成功，并从学术界辐射到了产业界。模型检验其基本原理实现为系统建立形式化模型，阐述所要验证的性质，然后用算法去检验该模型是否满足所述性质。模型检验提供一个完整的系统属性验证框架，模型检验的优点是模型检验能达到完全自动化的程度，只需用有穷状态模型和逻辑公式分别将系统实现和待验证的系统规范描述出来，之后的判断过程则完全可以由模型检验工具自动完成，不需要人的参与；模型检验过程总会以“是”或“否”的结果中止，当以“否”的结果中止时，说明设计或系统不满足某个给定的性质。此时一个违反性质的行为反例将会被给出，此反例将对理解错误的真正原因和修正错误提供线索。由于模型检验技术有以上优点，利用它对无线传感器网络进行同步机制的检验，在其设计阶段尽可能的找出错误。

动态规划是运筹学的一个分支，是求解决策过程最优化的数学方法。20世纪50年代初美国数学家R.E.Bellman等人在研究多阶段决策过程的优化问题时，提出了著名的最优化原理，把多阶段过程转化为一系列单阶段问题，利用各阶段之间的关系，逐个求解，创立了解决这类过程优化问题的新方法——动态规划。 动态规划算法通常用于求解具有某种最优性质的问题。在这类问题中，可能会有许多可行解。每一个解都对应于一个值，希望找到具有最优解的解。动态规划算法与分治法类似，其基本思想也是将待求解问题分解成若干个子问题，先求解子问题，然后从这些子问题的解得到原问题的解。与分治法不同的是，适合于用动态规划求解的问题，经分解得到子问题往往不是互相独立的。若用分治法来解这类问题，则分解得到的子问题数目太多，有些子问题被重复计算了很多次。如果能够保存已解决的子问题的答案，而在需要时再找出已求得的答案，这样就可以避免大量的重复计算，节省时间。可以用一个表来记录所有已解的子问题的答案。不管该子问题以后是否被用到，只要它被计算过，就将其结果填入表中。这就是动态规划法的基本思路。具体的动态规划算法多种多样，但它们具有相同的填表格式。 

发明内容

技术问题：本发明的目的是建立一种基于动态规划的传感器网络软件模型检验方法，解决传感器网络软件验证问题，克服验证在规模、动态性和资源约束等方面的挑战，通过发现传感器网络形式化模型的状态空间结构特点来缓解状态空间爆炸问题。

技术方案：本发明所述的基于动态规划的传感器网络软件模型检验方法包含如下过程：系统建模、模型预处理、模型性质验证。建模过程提供一个或一套较为抽象的时间状态自动机模型，化简与减枝模块减少自动机中对验证过程不产生影响的状态，实现时空复杂度一定程度的优化。在传感器网络软件模型检验中，利用动态规划，在模型化简与减枝的基础上，利用状态压缩的方法，使整个系统的验证过程时空复杂度达到进一步的优化，并将经过算法处理的数据输出转换为检验人员易懂的语言形式。

一、体系结构

1）本发明所述无线传感器网络是由部署在监测区域内的大量廉价微型传感器节点组成，通过无线通信形成一个多跳的自组织的网络系统，其目的在于协作地感知、采集、处理网络覆盖区域内感知对象的信息，并通过网络发送给观察者，从而使观察者得到对象的实时信息。

无线传感器网络节点数目多、分布密集、易失效、拓扑结构复杂、计算存储能力有限等特点对无线传感器网络协议提出了较高要求，因此无线传感器网络协议应具有健壮性、可扩展性和对有限资源的适应性的特点。对协议提出的高要求使得协议不可能再用工程直觉的方法来进行高质量设计。因此，网络协议分析成为必然趋势。

2）所述模型检验是利用形式化验证方法来自动验证有穷状态系统，证明一个系统一定没有某类错误的问题，首先建立形式化协议模型，然后通过检验数学模型判断协议是否存在错误。

3）所述动态规划用于有效解决模型验证过程中的空间爆炸问题，将验证过程分解成若干个子过程，求解子状态并保存，自底向上合并子过程，削减冗余状态，约束时空规模。

4）所述验证方法包括系统建模、模型预处理、模型性质验证等模块。

二、方法流程

1)系统建模

    11）分析无线传感器网络协议，列出协议所有常量和变量;

    12）列出节点所有可能状态;

所述状态是节点能够稳定维持的抽象化表述，包含一个或多个参数变量;

    13）列出节点各个状态之间转移条件，标注转移过程中参量变化，标记状态间的同步信号;

    14）根据转移条件，在各个状态节点之间建立有向边，建立状态自动机模型;

    15）用时序逻辑公式语言描述待验证的性质;

2）模型预处理

优化状态自动机模型，减少对验证过程不产生影响的状态，具体过程为：对状态自动机模型中的状态进行遍历，如果一个状态上没有时钟解释，并且其前驱迁移或者后继迁移都为空，则删除此状态，并对与此状态有关的迁移进行合并;

3）模型性质验证

31) 初始化根节点为所有模型中的初始状态的集合，当前节点为根节点;

32) 标记当前节点为已访问，由当前节点出发，根据状态转移条件，生成所有可能的临时目标状态，将所有状态添加为当前节点的子节点，并将未在状态空间树中出现过的状态放入集合A={ A₀，A₁，A₂，A₃……}中，同时将已出现过的状态节点标记为已访问;

33) 若A为空集，转步骤35);

34)  A非空，则以A₀为当前节点，转步骤32);

35)  寻找当前节点未被访问的兄弟节点，并以之为当前节点，转步骤32);

36)  若无法找到未被访问的兄弟节点，若父节点或当前节点为根节点，状态空间树生成完毕，转步骤37)；否则以父节点为当前节点，转步骤35);

37)  根据所要验证的性质，标记所有满足该性质的节点，并对该状态树进行深度优先搜索，验证其是否满足性质。

在已模型预处理的状态自动机模型上，对模型状态空间进行探测，采用基于动态规划思想的记忆化搜索方法建立一个用于性质验证的状态空间树，来确定模型拥有了某种属性或没有某种属性，如果没有这种属性还要提供一个反例以供调试。

将根据以上过程进行模型检验的最终结果展示出来，如果符合属性则告知用户满足的性质，反之则返回不满足的性质，并提供不满足性质的反例，将不满足性质的完整路径显示出来以供用户调试纠错。

有益效果：

1）本发明提供了一种基于动态规划的传感器网络模型检验方法，其完整的验证方法过程包括系统建模、模型预处理、模型性质验证，整个过程思路清晰完整，可读性强，尽量将晦涩难懂的相关技术概念、相关算法表述清晰，易于理解。

2）本发明中所述建模过程中，提供一个或一套较为抽象的时间状态自动机模型，能够将实际网络中的相关协议转化为数学化的模型形式。

3）本发明中所述模型化简与减枝模块减少自动机中的对验证过程不产生影响的状态，从而能够实现时空复杂度一定程度的优化。

4）本发明中所述动态规划思想方法，是在模型化建与减枝的基础上，利用状态压缩的方法，使得整个系统的验证过程时空复杂度达到进一步的优化效果。

附图说明

图1是模型检验基本流程。

图2是验证流程图。

图3是层次发现模型图。

图4是示例未优化状态空间树。

图5是示例已优化状态空间树。

图6是示例时序逻辑公式验证状态空间树。

具体实施方式

下面对本发明附图的某些实施例作更详细的描述。

根据附图1，本发明建立在模型检验技术的基础上，具体实施方式为：

1.系统建模

       现假设无线传感器网络采用层次结构，每个网络节点被赋予一个级别，根节点为0级，第i级的节点至少能够与一个第（i-1）级得节点通信；网络部署后，由根节点广播级别发现分组来启动层次发现阶段，级别发现分组包含节点的编号和级别；邻居节点收到分组后，将自己的级别设置为分组中的级别加1，然后广播新的级别发现分组；节点收到第i级节点的广播分组后，记录发送这个广播分组的节点编号，设置自己的级别为（i+1），广播级别为（i+1）的分组，这个过程持续到网络内每个节点都被赋予一个级别；节点一旦建立自己的级别，就忽略任何其他级别发现分组，防止网络产生洪泛拥塞。

1）分析无线传感器网络协议，列出所有常量和变量。

    常量包括节点编号（本例共2个节点，编号为0,1）。

    变量包括等待时间、节点所属层次记录数组。

    2）列出节点所有可能状态。状态即节点能够稳定维持一种抽象化表述，包含一个或多个参数变量。

    本例共有4个状态，分别为：等待态，初始化态，被发现态，广播态，各状态均包含变量等待时间。

    3）列出各个状态之间转移条件，标注转移过程中参量变化，标记状态间的同步信号。

    同步信号是层次发现信号数组，当i节点到达被发现态，向广播态转移时，向周围邻居节点发送该同步信号。

    转移条件为如下四个：其一，节点处于等待态时，若编号不为0，可转移至初始化态；其二，处于等待态，若编号为0，可转移至被发现态；其三，处于被发现态则无条件转移至广播态；其四，处于初始化态，收到邻居节点发出的层次发现同步信号时，转移至被发现态。

    4）根据转移条件，在各个状态节点之间建立有向边，建立状态自动机模型（见图3）。

    5）用时序逻辑公式描述待验证的性质p：0,1节点能在各种状态下均到达广播状态，描述为AF(p) （AF性质含义见图6，其中黑色节点表示该状态满足性质）。

2.模型预处理

优化状态自动机模型，减少对验证过程不产生影响的状态，具体过程为：对状态自动机模型中的状态进行遍历，如果一个状态上没有时钟解释，并且其前驱迁移或者后继迁移都为空，则删除此状态，并对与此状态有关的迁移进行合并。

3.模型性质验证

在已预处理的状态自动机模型上，对模型状态空间进行探测，采用基于动态规划思想的记忆化搜索方法建立一个用于性质验证的状态空间树，来确定模型拥有了某种属性或没有某种属性，如果没有这种属性还要提供一个反例以供调试。

根据系统建模模块所假设的协议，当前网络中有id=0,1两个传感器节点，0号为根节点。将两节点同时所处的状态描述作为状态空间树当中的状态节点。如状态（B,W）表示0节点处于广播态，同时1节点处于等待态。本例由（W,W）出发，根据条件转移产生的状态分支建立状态空间树。如（W,W）状态时，1节点由于条件满足转移至初始化态，则状态空间节点发生（W,W）→（W,I）转移；与此同时也可能发生（W,W）→（D,W）转移，产生分支。

按照不涉及动态规划思想进行验证，则验证过程中生成状态空间树（如图4）

其中W表示等待状态，即节点初始状态，I表示非根节点初始化状态，D表示被发现状态，B表示广播态。图中每个状态节点中左边字母代表0号节点状态，右边代表1号节点状态。

按照本模型性质验证模块提出的动态规划方法则验证过程中生成状态空间树（如图5）。

验证性质p：即在状态空间树中各分支均能转移到达（B，B）状态节点。验证过程中，若访问到已访问过的状态，即直接引用之前存储的结论，最终在状态空间树上验证出上述性质成立。