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

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

作　　者：冯晓宁[1] 王卓 张旭 

机构地区：[1]哈尔滨工程大学计算机科学与技术学院,哈尔滨150001 [2]哈尔滨工程大学水下机器人技术国防科技重点实验室,哈尔滨150001

出　　处：《吉林大学学报（工学版）》2015年第5期1565-1571,共7页Journal of Jilin University:Engineering and Technology Edition

基　　金：国家自然科学基金项目(61100006;61272184);黑龙江省自然科学基金项目(F201129)

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

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

分 类 号：TP393[自动化与计算机技术—计算机应用技术]