Technical Papers Parallel Session-II: Formal modeling and algorithm of subnet-based backup assigning in WSAN
Abstract/Description
Recently significant improvement in wireless sensor and actor networks has been made due to the increased interest of researchers. But still there is a need to overcome many operational challenges particularly in safety-critical and mission-critical large-scale applications. We propose a model of Subnet-Based Backup Assigning (SBBA) algorithm in wireless sensor and actor networks which assumes partitioning in WSAN into subnets. It identifies critical and non-critical nodes in each subnet and each critical node designates an appropriate backup to monitor the primary critical node and inter-actor connectivity is maintained within the subnet. In addition, it selects gateway node in each subnet to communicate with other subnets and a gateway node designates an appropriate backup to monitor the primary gateway node and inter-gateway connectivity is maintained among subnets. To prove the correctness of the proposed algorithm, this paper introduces a formal approach, i.e., VDM-SL for formal specification and analysis of SBBA algorithm in WSANs. We model topology and subnet of WSAN as dynamic graph and implement SBBA into a corresponding formal specification using VDM-SL. For the validation of the algorithm invariants are put on the data where it is required and for the correct operation of communication pre and post conditions are defined. The specification of the SBBA algorithm is verified, analyzed and validated using VDM-SL toolbox.
Keywords
Wireless sensor and actor network, Formal specification, Model analysis, VDM-SL, Failure recovery
Location
C-10, AMAN CED
Session Theme
Technical Papers Parallel Session-II (Networks-1)
Session Type
Parallel Technical Session
Session Chair
Dr. Amir Qayyum
Start Date
12-12-2015 3:50 PM
End Date
12-12-2015 4:10 PM
Recommended Citation
Afzaal, H., & Zafar, N. A. (2015). Technical Papers Parallel Session-II: Formal modeling and algorithm of subnet-based backup assigning in WSAN. International Conference on Information and Communication Technologies. Retrieved from https://ir.iba.edu.pk/icict/2015/2015/12
COinS
Technical Papers Parallel Session-II: Formal modeling and algorithm of subnet-based backup assigning in WSAN
C-10, AMAN CED
Recently significant improvement in wireless sensor and actor networks has been made due to the increased interest of researchers. But still there is a need to overcome many operational challenges particularly in safety-critical and mission-critical large-scale applications. We propose a model of Subnet-Based Backup Assigning (SBBA) algorithm in wireless sensor and actor networks which assumes partitioning in WSAN into subnets. It identifies critical and non-critical nodes in each subnet and each critical node designates an appropriate backup to monitor the primary critical node and inter-actor connectivity is maintained within the subnet. In addition, it selects gateway node in each subnet to communicate with other subnets and a gateway node designates an appropriate backup to monitor the primary gateway node and inter-gateway connectivity is maintained among subnets. To prove the correctness of the proposed algorithm, this paper introduces a formal approach, i.e., VDM-SL for formal specification and analysis of SBBA algorithm in WSANs. We model topology and subnet of WSAN as dynamic graph and implement SBBA into a corresponding formal specification using VDM-SL. For the validation of the algorithm invariants are put on the data where it is required and for the correct operation of communication pre and post conditions are defined. The specification of the SBBA algorithm is verified, analyzed and validated using VDM-SL toolbox.
