Algorithm and Formal Specification of Subnet- Based Communication in WSANs

Hamra Afzaal ； Nazir Ahmad Zafar

《Bahria University Journal of Information & Communication Technologies》 9卷S期 (2016/09) Pp. 14-23

摘要

Recently Wireless Sensor and Actor Networks (WSANs) have drawn increased interest of researchers due to a large number of applications in large scale mission and safetycritical systems. Although significant improvements have been made in WSANs but still there is a need to overcome many challenges. Energy management is a major challenge in WSANs, that's why we present an energy efficient model of Subnet-Based Communication (SBC) algorithm in WSANs. The proposed model pursues WSAN and partitions into subnets. Firstly, in each subnet it proactively distinguishes between critical and non-critical nodes. A critical node selects suitable neighbor as a backup within the subnet for its monitoring and maintaining the inter-actor connectivity within the subnet. Then it chooses one gateway node from each subnet for the continuous communication among subnets and gateway nodes continuously communicate intelligently using Open Shortest Path First (OSPF) routing protocol. Backups are assigned to the gateway nodes to maintain the inter-gateway connectivity among subnets. VDM-SL is introduced as a formal technique for the implementation of SBC algorithm. Validation and verification of the algorithm are done through VDM-SL toolbox which proves its correctness.

關鍵字

Formal Verification and Validation ； Open Shortest Path First ； Subnet-Based Communication ； WSAN ； VDM-SL