Abstract
Wireless sensor and actor networks (WSAN) are captivating significant attention because of their suitability for safety-critical applications. Efficient actor placement in such applications is extremely desirable to perform effective and timely action across the deployment region. Nonetheless, harsh application environment inherently favors random placement of actors that leads to high concentration deployment and strangles coverage. Moreover, most of the published schemes lack rigorous validation and entirely rely on informal techniques (e.g., simulation) for evaluating nonfunctional properties of algorithms. This paper presents a localized movement control actor relocation (MCAR) algorithm that strives to improve connected coverage while minimizing movement overhead. MCAR pursues post-deployment actor repositioning in such a way that actors repel each other for better coverage while staying connected. We employ complementary formal and informal techniques for MCAR verification and validation. We model WSAN as a dynamic graph and transform MCAR to corresponding formal specification using Z notation. The resulting specification is analyzed and validated using Z eves tool. We simulate the specification to quantitatively demonstrate the efficiency of MCAR. Simulation results confirm the efficiency of MCAR in terms of movement overhead and connected coverage compared to contemporary schemes. The results show that MCAR can reduce distance movement up to 32 % while improving coverage up to 29 % compared to published schemes.