SDL based validation of a node monitoring protocol

TL;DR

This paper proposes an SDL-based validation model for a node monitoring protocol in mobile ad hoc networks, verifying its correctness and behavior under various conditions using formal methods.

Contribution

It introduces a novel SDL-based validation approach for node monitoring protocols, including static and mobile agent models, with formal verification and visualization techniques.

Findings

Verified protocol properties with no deadlocks or improper states

Used reachability graph for exhaustive state analysis

MSC diagrams illustrate system behavior under different scenarios

Abstract

Mobile ad hoc network is a wireless, self-configured, infrastructureless network of mobile nodes. The nodes are highly mobile, which makes the application running on them face network related problems like node failure, link failure, network level disconnection, scarcity of resources, buffer degradation, and intermittent disconnection etc. Node failure and Network fault are need to be monitored continuously by supervising the network status. Node monitoring protocol is crucial, so it is required to test the protocol exhaustively to verify and validate the functionality and accuracy of the designed protocol. This paper presents a validation model for Node Monitoring Protocol using Specification and Description Llanguage (SDL) using both Static Agent (SA) and Mobile Agent (MA). We have verified properties of the Node Monitoring Protocol (NMP) based on the global states with no exits, deadlock states or proper termination states using reachability graph. Message Sequence Chart (MSC) gives an intuitive understanding of the described system behavior with varying node density and complex behavior etc.