  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.
