Formalising Sensor Topologies for Target Counting

TL;DR

This paper introduces a formal logical model to analyze sensor topologies for target counting, enabling verification and potential improvements of algorithms in static and mobile sensor networks.

Contribution

It develops a first-order logic framework for specifying sensor coverage relations and formalizes the correctness of a target counting algorithm, addressing ambiguities and extensions.

Findings

Formal logic specification of sensor topologies

Verification of counting algorithm correctness

Framework for extending to mobile sensors and temporal data

Abstract

We present a formal model developed to reason about topologies created by sensor ranges. This model is used to formalise the topological aspects of an existing counting algorithm to estimate the number of targets in the area covered by the sensors. To that end, we present a first-order logic tailored to specify relations between parts of the space with respect to sensor coverage. The logic serves as a specification language for Hoare-style proofs of correctness of the topological computations of the algorithm, which uncovers ambiguities in their results. Subsequently, we extend the formal model as a step towards improving the estimation of the algorithm. Finally, we sketch how the model can be extended to take mobile sensors and temporal aspects into account.