Formalising Nondeterministic Communication in Wireless Sensor Networks Using CSP
Chapter
Accepted version
Åpne
Permanent lenke
https://hdl.handle.net/11250/3026416Utgivelsesdato
2021Metadata
Vis full innførselSamlinger
Originalversjon
Published in: 2021 10th Mediterranean Conference on Embedded Computing (MECO) 10.1109/MECO52532.2021.9460193Sammendrag
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.