- Title
- Formal verification and validation of a movement control actor relocation algorithm for safety–critical applications
- Creator
- Imran, Muhammad; Zafar, Nazir; Alnuem, Mohammed; Aksoy, Mehmet; Vasilakos, Athanasios
- Date
- 2016
- Type
- Text; Journal article
- Identifier
- http://researchonline.federation.edu.au/vital/access/HandleResolver/1959.17/186393
- Identifier
- vital:16890
- Identifier
-
https://doi.org/10.1007/s11276-015-0962-8
- Identifier
- ISBN:1022-0038 (ISSN)
- 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. © 2015, Springer Science+Business Media New York.
- Publisher
- Springer New York LLC
- Relation
- Wireless Networks Vol. 22, no. 1 (2016), p. 247-265
- Rights
- All metadata describing materials held in, or linked to, the repository is freely available under a CC0 licence
- Rights
- Copyright @ Springer Science+Business Media New York 2015
- Subject
- 4006 Communications engineering; 4606 Distributed computing and systems software; Connected coverage; Formal specification; Movement control actor relocation; WSANs; Z notation
- Reviewed
- Funder
- This work was supported by the Research Center of College of Computer and Information Sciences, King Saud University, Riyadh, Saudi Arabia, through the Research Project No. RC131026.
- Hits: 373
- Visitors: 319
- Downloads: 0
| Thumbnail | File | Description | Size | Format |
|---|