Authors: Admar Ajith Kumar Somappa; Lars M. Kristensen; Andreas Prinz
Addresses: Department of Electrical Engineering, Western Norway University of Applied Sciences, Sogndal, Norway ' Department of Computing, Mathematics and Physics, Western Norway University of Applied Sciences, Sogndal, Norway ' Department of Information and Communication Technology, University of Agder, 4630 Kristiansand S, Norway
Abstract: Wireless sensor and actuator networks (WSANs) rely on MAC protocols to coordinate access to the wireless medium access and for managing the radio unit on each device. The dual-mode adaptive MAC (DMAMAC) protocol is a recently proposed protocol designed to reduce the energy consumption of the radio communication in WSANs. The DMAMAC protocol targets the industrial WSANs used for real-time process control. At its core, DMAMAC exploits the distinction between transient and steady of the controlled plant process to dynamically adapt the MAC superframe structure and thereby conserve energy. The switch between steady and transient mode of operation is a safety-critical part of the protocol. The contribution of this paper is to develop a rigorous specification of the DMAMAC protocol using timed automata and the supporting Uppaal software tool. The Uppaal tool is also used to verify key functional and real-time properties of the protocol. Finally, we have used execution sequences from the formal specification model to validate an OMNET simulation model used for performance evaluation of DMAMAC, and to validate a nesC implementation of the protocol on the TinyOS platform.
Keywords: verification; validation; simulation; deployment; industrial wireless sensor network; MAC protocol; Uppaal.
International Journal of Critical Computer-Based Systems, 2018 Vol.8 No.2, pp.108 - 140
Accepted: 08 Jun 2018
Published online: 09 Nov 2018 *