dc.contributor.author | Andersen, Sondre Ninive | |
dc.contributor.author | Espe, Asbjørn Engmark | |
dc.contributor.author | Hendseth, Sverre | |
dc.contributor.author | Mathisen, Geir | |
dc.date.accessioned | 2022-10-17T12:29:19Z | |
dc.date.available | 2022-10-17T12:29:19Z | |
dc.date.created | 2021-07-02T13:13:01Z | |
dc.date.issued | 2021 | |
dc.identifier.citation | Published in: 2021 10th Mediterranean Conference on Embedded Computing (MECO) | en_US |
dc.identifier.isbn | 978-1-6654-3912-1 | |
dc.identifier.uri | https://hdl.handle.net/11250/3026416 | |
dc.description.abstract | 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. | en_US |
dc.language.iso | eng | en_US |
dc.publisher | IEEE | en_US |
dc.relation.ispartof | 2021 10th Mediterranean Conference on Embedded Computing (MECO) | |
dc.title | Formalising Nondeterministic Communication in Wireless Sensor Networks Using CSP | en_US |
dc.type | Chapter | en_US |
dc.description.version | acceptedVersion | en_US |
dc.rights.holder | © 2021 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works. | en_US |
dc.identifier.doi | 10.1109/MECO52532.2021.9460193 | |
dc.identifier.cristin | 1920057 | |
cristin.ispublished | true | |
cristin.fulltext | postprint | |
cristin.qualitycode | 1 | |