Formal verification and validation of a movement control actor relocation algorithm for safety–critical applications

Imran, M; Zafar, NA; Alnuem, MA; Aksoy, MS; Vasilakos, AV

Formal verification and validation of a movement control actor relocation algorithm for safety–critical applications

Imran, M Zafar, NA Alnuem, MA Aksoy, MS Vasilakos, AV

Permalink

Publisher:: SPRINGER
Publication Type:: Journal Article
Citation:: Wireless Networks, 2016, 22, (1), pp. 247-265
Issue Date:: 2016-01-01

Closed Access

	Filename	Description	Size
	Imran2016_Article_FormalVerificationAndValidatio.pdf	Published version	2.6 MB	Adobe PDF	View/Open

Copyright Clearance Process

Recently Added
In Progress
Closed Access

This item is closed access and not available.

Full metadata record

Field	Value	Language
dc.contributor.author	Imran, M
dc.contributor.author	Zafar, NA
dc.contributor.author	Alnuem, MA
dc.contributor.author	Aksoy, MS
dc.contributor.author	Vasilakos, AV
dc.date.accessioned	2022-08-12T04:54:03Z
dc.date.available	2022-08-12T04:54:03Z
dc.date.issued	2016-01-01
dc.identifier.citation	Wireless Networks, 2016, 22, (1), pp. 247-265
dc.identifier.issn	1022-0038
dc.identifier.issn	1572-8196
dc.identifier.uri	http://hdl.handle.net/10453/160020
dc.description.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.
dc.language	English
dc.publisher	SPRINGER
dc.relation.ispartof	Wireless Networks
dc.relation.isbasedon	10.1007/s11276-015-0962-8
dc.rights	info:eu-repo/semantics/closedAccess
dc.subject	0805 Distributed Computing, 0906 Electrical and Electronic Engineering, 1005 Communications Technologies
dc.subject.classification	Networking & Telecommunications
dc.title	Formal verification and validation of a movement control actor relocation algorithm for safety–critical applications
dc.type	Journal Article
utslib.citation.volume	22
utslib.for	0805 Distributed Computing
utslib.for	0906 Electrical and Electronic Engineering
utslib.for	1005 Communications Technologies
pubs.organisational-group	/University of Technology Sydney
pubs.organisational-group	/University of Technology Sydney/Faculty of Engineering and Information Technology
pubs.organisational-group	/University of Technology Sydney/Faculty of Engineering and Information Technology/School of Electrical and Data Engineering
utslib.copyright.status	closed_access	*
dc.date.updated	2022-08-12T04:54:01Z
pubs.issue	1
pubs.publication-status	Published
pubs.volume	22
utslib.citation.issue	1

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.

Please use this identifier to cite or link to this item:

http://hdl.handle.net/10453/160020