吉林大学学报(工学版) ›› 2015, Vol. 45 ›› Issue (5): 1565-1571.doi: 10.13229/j.cnki.jdxbgxb201505027

• • 上一篇    下一篇

基于L-π演算的WSN路由协议形式化方法

冯晓宁1, 王卓2, 张旭1   

  1. 1.哈尔滨工程大学 计算机科学与技术学院,哈尔滨 150001;
    2.哈尔滨工程大学 水下机器人技术国防科技重点实验室,哈尔滨150001
  • 收稿日期:2013-12-19 出版日期:2015-09-01 发布日期:2015-09-01
  • 作者简介:冯晓宁(1976-）,男,副教授.研究方向:建模与仿真,无线传感器网络,并行计算.E-mail:fengxiaoning@hrbeu.edu.cn
  • 基金资助:
    国家自然科学基金项目(61100006,61272184); 黑龙江省自然科学基金项目(F201129)

Formal method for routing protocol of WSN based on L-π calculus

FENG Xiao-ning1, WANG Zhuo2, ZHANG Xu1   

  1. 1.College of Computer Science and Technology, Harbin Engineering University, Harbin 150001,China;
    2.National Key Laboratory of Science and Technology on Autonomous Underwater Vehicle, Harbin Engineering University, Harbin 150001, China
  • Received:2013-12-19 Online:2015-09-01 Published:2015-09-01
  • Supported by:
    ; 该过程负责广播election消息,然后进入等待确认消息的状态awaitAck,awaitAck的描述为:; awaitAck(a→)=; chan(ack(Y)).processAck(id,chan,pchan,init,; elec,energy,Y,)+[init=0]pchan(ˉack; 在该状态中节点会非确定地选择下述三种情况执行:①若节点的init为0,说明该节点为普通节点,那么它通过与父节点的通道单播发送(ack message)消息以及它已知的最大能量发送到父节点,并进入node状态;②若节点的init为1,说明节点为发起节点(initNode),此时它需要广播应成为簇头节点的id到其邻居节点,并将elec的值置为0,以标示退出选择过程,然后进入node状态;节点还有可能收到子节点发送的(ack message)以及子节点已知的最大能量值,节点将参数maxenergy用收到的最大能量值替换并进入对(ack message)消息确认的状态processAck,processAck的描述为:; processAck(a→)=; [maxenergy>=energy]awaitAck(a→)+; [maxenergy<energy]; awaitAck(id,chan,pchan,init,elec,energy,energy); 在该状态中,若节点已知的最大能量大于它本身的能量,节点保存这个信息并返回(awaitAck)状态;否则,节点会用本身的能量值替换maxenergy参数,然后返回(awaitAck)状态。; node进程中还有processLeader过程,它的描述为:; initNode(a→)=broˉelection.awaitAck(a→); 它负责广播发送election消息,然后进入等待状态。

RICH HTML

0   

PDF (PC)

270

摘要： 针对无线传感器网络路由协议形式化描述与验证的问题,提出了一种形式化方法L-π演算。定义了L-π演算的语法,形式化描述无线传感器节点的广播与单播的通信行为。定义了相应的结构同余,描述了节点表达式的非顺序性。定义了相应的迁移规则,提供了路由协议形式化模型的动态推演功能。通过对无线传感器网络簇头选择协议的描述展现了L-π演算的能力。通过无线传感器网络簇头选择协议的验证实验说明了该方法能有效验证无线传感网络路由协议。

关键词: 计算机软件, 无线传感器网络, 路由协议, 形式化方法, L-π, 演算

Abstract: A process calculus called L-π calculus was proposed to solve the issue of formal specification and verification for Wireless Sensor Network (WSN) routing protocol. The calculus can capture the characteristics of WSN, including the limit transmission range and broadcast communication. The defined syntax of the L-π calculus describes the network from the perspective of node. Structural congruence defined in L-π describes the non-sequential of node expression. Transitional rules of L-π calculus in terms of labeled transition systems are also defined to provide the function of dynamic deduction. After the definition of L-π calculus, a leader election protocol is described to demonstrate the description ability of the calculus. Finally, the calculus is illustrated by developing and analyzing formal models of the leader election protocol for WSN.

Key words: computer software, wireless sensor network, routing protocol, formal method, L-π, calculus

中图分类号: 

  • TP393
[1] 孙利民,李建中,陈渝,等.无线传感器网络[M].北京:清华大学出版社,2009.
[2] Godskesen J C. A calculus for mobile ad hoc networks[C]∥Coordination Models and Languages. Springer Berlin Heidelberg, 2007: 132-150.
[3] Merro M. An observational theory for mobile ad hoc networks[J]. Electronic Notes in Theoretical Computer Science, 2007, 173: 275-293.
[4] Mezzetti N, Sangiorgi D. Towards a calculus for wireless systems[J]. Electronic Notes in Theoretical Computer Science, 2006, 158: 331-353.
[5] Singh A, Ramakrishnan C R, Smolka S A. A process calculus for mobile ad hoc networks[J]. Science of Computer Programming, 2010, 75(6): 440-469.
[6] Orfanus D, Heimfarth T, Wagner F R. Process algebra to model Self-Organizing behavior in wireless sensor networks[C]∥Ultra Modern Telecommunications & Workshops, 2009. ICUMT'09. International Conference on, IEEE, 2009:1-6.
[7] Liu S, Zhao Y, Zhu H, et al. A calculus for mobile Ad Hoc networks from a group probabilistic Perspective[C]∥High-Assurance Systems Engineering (HASE), 2011 IEEE 13th International Symposium on. IEEE, 2011: 157-162.
[8] Thong V T, Buttyán L, Dvir A. On formal and automatic security verification of WSN transport protocols[J]. International Scholarly Research Notices,2014:891467.
[9] Gallina L, Rossi S. A process calculus for energy‐aware multicast communications of mobile ad hoc networks[J]. Wireless Communications and Mobile Computing, 2013, 13(3): 296-312.
[10] Milner R. 通信与移动系统[M]. 林惠民,柳欣欣,刘佳,等译.北京:清华大学出版社,2009:88.
[11] Vasudevan S, Kurose J, Towsley D. Design and analysis of a leader election algorithm for mobile ad hoc networks[C]∥Network Protocols,2004,ICNP,2004,Proceedings of the 12th IEEE International Conference on. IEEE,2004: 350-360.
[12] Yang P, Dong Y, Ramakrishnan C R, et al. A Provably correct Compiler for Efficient Model Checking of Mobile Processes[M].Practical Aspects of Declarative Languages. Springer Berlin Heidelberg, 2005: 113-127.
[1] 董颖, 崔梦瑶, 吴昊, 王雨后. 基于能量预测的分簇可充电无线传感器网络充电调度[J]. 吉林大学学报(工学版), 2018, 48(4): 1265-1273.
[2] 张维维, 何家峰, 高国旺, 任丽莉, 申铉京. 基于博弈论的无线Mesh网络路由与信道分配联合优化算法[J]. 吉林大学学报(工学版), 2018, 48(3): 887-892.
[3] 马健, 樊建平, 刘峰, 李红辉. 面向对象软件系统演化模型[J]. 吉林大学学报(工学版), 2018, 48(2): 545-550.
[4] 刘洲洲, 彭寒. 基于节点可靠度的无线传感器网络拓扑控制算法[J]. 吉林大学学报(工学版), 2018, 48(2): 571-577.
[5] 董坚峰, 张玉峰, 戴志强. 改进的基于狄利克雷混合模型的推荐算法[J]. 吉林大学学报(工学版), 2018, 48(2): 596-604.
[6] 罗养霞, 郭晔. 基于数据依赖特征的软件识别[J]. 吉林大学学报(工学版), 2017, 47(6): 1894-1902.
[7] 于斌斌, 武欣雨, 初剑峰, 胡亮. 基于群密钥协商的无线传感器网络签名协议[J]. 吉林大学学报(工学版), 2017, 47(3): 924-929.
[8] 董颖, 周占颖, 苏真真, 徐洋, 钱志鸿. 基于路由信息的无线传感器网络跨层MAC协议[J]. 吉林大学学报(工学版), 2017, 47(2): 647-654.
[9] 应欢, 王东辉, 武成岗, 王喆, 唐博文, 李建军. 适用于商用系统环境的低开销确定性重放技术[J]. 吉林大学学报(工学版), 2017, 47(1): 208-217.
[10] 朱海洋, 张合, 马少杰. 增强型超声波周向旋转扫描节点参数优化[J]. 吉林大学学报(工学版), 2017, 47(1): 262-267.
[11] 李勇, 黄志球, 王勇, 房丙午. 基于多源数据的跨项目软件缺陷预测[J]. 吉林大学学报(工学版), 2016, 46(6): 2034-2041.
[12] 刘洲洲, 王福豹. 改进的离散混合蛙跳算法压缩感知信号重构及应用[J]. 吉林大学学报(工学版), 2016, 46(4): 1261-1268.
[13] 张婧, 刘衍珩, 张晋东, 孙庚. 无线传感器网络簇半径自适应调整策略[J]. 吉林大学学报(工学版), 2016, 46(3): 876-883.
[14] 王念滨, 祝官文, 周连科, 王红卫. 支持高效路径查询的数据空间索引方法[J]. 吉林大学学报(工学版), 2016, 46(3): 911-916.
[15] 特日跟, 江晟, 李雄飞, 李军. 基于整数数据的文档压缩编码方案[J]. 吉林大学学报(工学版), 2016, 46(1): 228-234.
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
No Suggested Reading articles found!
版权所有 © 《吉林大学学报(工学版)》编辑部
地址：长春市人民大街5988号　电话：+86-431-85095297　传真：+86-431-85094074　E-mail: xbgxb@jlu.edu.cn
本系统由北京玛格泰克科技发展有限公司设计开发