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

(19)中华人民共和国国家知识产权局

	(12)发明专利说明书
		(10)申请公布号 CN 103220685 A (43)申请公布日 2013.07.24

(21)申请号 CN201310140565.5

(22)申请日 2013.04.22

(71)申请人南京邮电大学

地址 210003 江苏省南京市鼓楼区新模范马路66号

(72)发明人陈志黄洵松毛博曹壹岳文静曾雅芸迟文东

(74)专利代理机构南京经纬专利商标代理有限公司

代理人叶连生

(51)Int.CI

H04W16/18

H04W24/00

H04W84/18

权利要求说明书说明书幅图

(54)发明名称

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

(57)摘要

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

法律状态

法律状态公告日	法律状态信息	法律状态
2023-03-28	未缴年费专利权终止IPC(主分类):H04W16/18专利号:ZL2013101405655申请日:20130422授权公告日:20160330	专利权的终止

权利要求说明书

1.一种基于动态规划的传感器网络软件模型检验方法，其特征在于该方法包括以下步骤：

1)系统建模

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

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

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

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

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

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

2）模型预处理

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

3）模型性质验证

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

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

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

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

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

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

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

2.根据权利要求1所述的基于动态规划的传感器网络软件模型检验方法，其特征在于在已模型预处理的状态自动机模型上，对模型状态空间进行探测，采用基于动态规划思想的记忆化搜索方法建立一个用于性质验证的状态空间树，来确定模型拥有某种属性或没有某种属性，如果没有这种属性还要提供一个反例以供调试。

本文发布于:2024-09-20 10:42:55，感谢您对本站的认可！

本文链接：https://www.17tex.com/xueshu/802312.html

上一篇：一种交通时空过程建模管理方法及装置[发明专利]

下一篇：一种绳驱动连续型机械臂的三维静力学建模方法

标签：状态模型节点验证方法性质

留言与评论（共有 0 条评论）