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

Previous Articles     Next Articles

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)

260

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

CLC Number: 

  • 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] ZHANG Wei-wei, HE Jia-feng, GAO Guo-wang, REN Li-li, SHEN Xuan-jing. Wireless Mesh network routing and channel allocation union optimization algorithm based on game theory [J]. 吉林大学学报(工学版), 2018, 48(3): 887-892.
[2] MA Jian, FAN Jian-ping, LIU Feng, LI Hong-hui. The evolution model of objective-oriented software system [J]. 吉林大学学报(工学版), 2018, 48(2): 545-550.
[3] LIU Zhou-zhou, PENG Han. Topology control algorithm based on node reliability in WSN [J]. 吉林大学学报(工学版), 2018, 48(2): 571-577.
[4] LUO Yang-xia, GUO Ye. Software recognition based on features of data dependency [J]. 吉林大学学报(工学版), 2017, 47(6): 1894-1902.
[5] TANG Kun, SHI Rong-hua. Detection of wireless sensor network failure area based on butterfly effect signal [J]. 吉林大学学报(工学版), 2017, 47(6): 1939-1948.
[6] YU Bin-bin, WU Xin-yu, CHU Jian-feng, HU Liang. Signature protocol for wireless sensor network based on group key agreement [J]. 吉林大学学报(工学版), 2017, 47(3): 924-929.
[7] DONG Ying, ZHOU Zhan-ying, SU Zhen-zhen, XU Yang, QIAN Zhi-hong. Cross-layer MAC protocol based on routing information for WSN [J]. 吉林大学学报(工学版), 2017, 47(2): 647-654.
[8] YING Huan, WANG Dong-hui, WU Cheng-gang, WANG Zhe, TANG Bo-wen, LI Jian-jun. Efficient deterministic replay technique on commodity system environment [J]. 吉林大学学报(工学版), 2017, 47(1): 208-217.
[9] ZHU Hai-yang, ZHANG He, MA Shao-jie. Parameter optimization of enhanced ultrasonic circumferential scanning node in WSN [J]. 吉林大学学报(工学版), 2017, 47(1): 262-267.
[10] LI Yong, HUANG Zhi-qiu, WANG Yong, FANG Bing-wu. New approach of cross-project defect prediction based on multi-source data [J]. 吉林大学学报(工学版), 2016, 46(6): 2034-2041.
[11] LIU Zhou-zhou, WANG Fu-bao. Improvement of discrete shuffled frog-leaping algorithm and application in compressed sensing reconstruction [J]. 吉林大学学报(工学版), 2016, 46(4): 1261-1268.
[12] ZHANG Jing, LIU Yan-heng, ZHANG Jin-dong, SUN Geng. Cluster size adaptive adjustable strategy for wireless sensor networks [J]. 吉林大学学报(工学版), 2016, 46(3): 876-883.
[13] WANG Nian-bin, ZHU Guan-wen, ZHOU Lian-ke, WANG Hong-wei. Novel dataspace index for efficient processing of path query [J]. 吉林大学学报(工学版), 2016, 46(3): 911-916.
[14] TE Ri-gen, JIANG Sheng, LI Xiong-fei, LI Jun. Document compression scheme based on integer data [J]. 吉林大学学报(工学版), 2016, 46(1): 228-234.
[15] KANG Hui, WANG Jia-qi, MEI Fang. A parallel programming language based on Pi-calculus [J]. 吉林大学学报(工学版), 2016, 46(1): 235-241.
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
No Suggested Reading articles found!
Copyright © Journal of Jilin University(Engineering and Technology Edition), All Rights Reserved.
Tel: +86-431-85095297　Fax: +86-431-85094074　E-mail: xbgxb@jlu.edu.cn
Powered by Beijing Magtech Co. Ltd