Title: Model-based specification and validation of the dual-mode adaptive MAC protocol

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.

DOI: 10.1504/IJCCBS.2018.096190

International Journal of Critical Computer-Based Systems, 2018 Vol.8 No.2, pp.108 - 140

Accepted: 08 Jun 2018
Published online: 15 Nov 2018 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article