Imperial College London
Portrait Picture

ProfessorJulieMcCann

Faculty of Engineering, Department of Computing

Vice-Dean (Research) for the Faculty of Engineering
 
 
 
//

Contact

 

+44 (0)20 7594 8375j.mccann Website

 
 
//

Assistant

 

Miss Teresa Ng +44 (0)20 7594 8300

 
//

Location

 

260ACE ExtensionSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@article{Webster:2019:10.14279/tuj.eceasst.76.1078,
author = {Webster, M and Breza, M and Dixon, C and Fisher, M and McCann, J},
doi = {10.14279/tuj.eceasst.76.1078},
journal = {Electronic Communications of the EASST},
title = {Formal verification of synchronisation, gossip and environmental effects for wireless sensor networks},
url = {http://dx.doi.org/10.14279/tuj.eceasst.76.1078},
volume = {76},
year = {2019}
}
Download

RIS format (EndNote, RefMan)

TY  - JOUR
AB  - The Internet of Things (IoT) promises a revolution in the monitoring and control of a wide range of applications, from urban water supply networks and precision agriculture food production, to vehicle connectivity and healthcare monitoring. For applications in such critical areas, control software and protocols for IoT systems must be verified to be both robust and reliable. Two of the largest obstacles to robustness and reliability in IoT systems are effects on the hardware caused by environmental conditions, and the choice of parameters used by the protocol. In this paper we use probabilistic model checking to verify that a synchronisation and dissemination protocol for Wireless Sensor Networks (WSNs) is correct with respect to its requirements, and is not adversely affected by the environment. We show how the protocol can be converted into a logical model and then analysed using the probabilistic model-checker, PRISM. Using this approach we prove under which circumstances the protocol is guaranteed to synchronise all nodes and disseminate new information to all nodes. We also examine the bounds on synchronisation as the environment changes the performance of the hardware clock, and investigate the scalability constraints of this approach.
AU  - Webster,M
AU  - Breza,M
AU  - Dixon,C
AU  - Fisher,M
AU  - McCann,J
DO  - 10.14279/tuj.eceasst.76.1078
PY  - 2019///
SN  - 1863-2122
TI  - Formal verification of synchronisation, gossip and environmental effects for wireless sensor networks
T2  - Electronic Communications of the EASST
UR  - http://dx.doi.org/10.14279/tuj.eceasst.76.1078
UR  - http://hdl.handle.net/10044/1/71828
VL  - 76
ER  -
Download