Valkov, I. and Miller, A. (2019) Using Model Checking in the Design of a Sensor Network Protocol. In: 26th Automated Reasoning Workshop (ARW

We investigate how the PRISM and Alloy model checkers can be used in the design of a sensor network communication protocol. We introduce the two model checkers and illustrate how Alloy can be used to specify and analyse an existing communication protocol WirelessHART. We then propose how PRISM and Alloy will be used in the design of a new protocol, Ctrl-MAC, which is currently being developed as part of an EPSRC funded program grant, S4: Science of Sensor System Software. The aim is to exploit the strengths of each approach to allow us to select parameters and configurations to optimise the protocol.