Formalising Nondeterministic Communication in Wireless Sensor Networks Using CSP

Using communicating sequential processes (CSP), this paper presents a model for wireless sensor networks (WSNs) to be used for formal verification of communication reliability in mesh networks. Process models are derived for sensor nodes and communication links, introducing nondeterminism in order to capture the unreliability inherent in wireless communication. It is shown that a guarantee may be issued concerning the CSP model's worst-case performance in terms of packet corruption. This guarantee is substantiated by transformation of the model, employing a series of operations introduced to simplify the network while preserving worst-case performance. The end result is a formal proof of the entire network's worst-case reliability. As long as the nondeterminism of the communication links is modelled with care, the packet corruption rate through the network will be equal to or better than the worst-case performance of its most deterministic path.