Title: Spatial properties verification approach of wireless sensor networks using model checking

Authors: Jia Wang; Jun Niu; Zheke Yuan; Fan Fei

Addresses: Faculty of Electrical Engineering and Computer Science, Ningbo University, Ningbo 315200, China ' Faculty of Electrical Engineering and Computer Science, Ningbo University, Ningbo 315200, China; Key Laboratory of Embedded System and Service Computing, Tongji University, Shanghai 201804, China ' Faculty of Electrical Engineering and Computer Science, Ningbo University, Ningbo 315200, China ' Faculty of Electrical Engineering and Computer Science, Ningbo University, Ningbo 315200, China

Abstract: Reasonable spatial deployment of wireless sensor networks (WSNs) can extend their life cycles and enhance the reliability of the systems relying on them. The spatial layouts of WSNs need to be strictly verified to ensure they satisfy desired requirements. Model checking has made some progress in verifying spatial properties of WSNs, and the spatial logic for closure space (SLCS) can characterise some spatial specifications of WSNs. However, SLCS is imperfect in characterising and reasoning about some quantitative properties of WSNs. In this paper, we firstly propose a novel WSN spatial model, namely quantitative closure space model (QCSM), to model WSNs with quantitative descriptions. Then, we use the improved SLCS logic, which is extended with a novel degree-correlation operator to enrich the expressiveness of SLCS, to characterise more kinds of spatial specifications of WSNs. Experiments indicate that our approach can automatically and effectively verify some complex spatial specifications of WSNs.

Keywords: wireless sensor networks; WSNs; spatial deployment; spatial specification; modal logic; spatial logic for closure space; SLCS; quantitative closure space model; QCSM; degree-correlation operator.

DOI: 10.1504/IJSNET.2022.127109

International Journal of Sensor Networks, 2022 Vol.40 No.3, pp.175 - 189

Received: 06 Jan 2022
Received in revised form: 18 May 2022
Accepted: 06 Jun 2022
Published online: 22 Nov 2022 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article