Vers un protocole TDMA multi-débit à diversité spatiale pour les réseaux de capteurs et d’actionneurs sans fil : modélisation et vérification

Abstract

At the core of many today’s industrial applications are the wireless sensor networks (WSNs) and wireless sensor and actuator networks (WSANs). WSNs and WSANs have led to the development of industrial wireless sensor networks (IWSNs) and industrial wireless sensor and actuator networks (IWSANs). These networks play a central role of connecting machines, parts, products, and humans and create a diverse set of new applications to support intelligent and autonomous decision making. For each application, communication protocols should be tailored to comply all requirements specific to that application. Requirements could be specified in terms of end-to-end delay, throughput flexibility, etc. In order to achieve compliance with such requirement, choices should be made during the design process regarding MAC access and routing algorithm. We propose in this paper a multi-rate TDMA protocol with spatial re-use. The protocol proposed in this work is designed to fit heterogeneous networks where different types of sensor and actuators coexist. We give first a formal model of the protocol using timed automata paradigm and then we carry out a formal verification of basic properties upon the model with the UPPAAL model-checker.