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



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.


wireless sensor and actuator networks, wireless sensor networks, spatial TDMA, multi-rate TDMA, formal modeling, communication protocol

Full Text:



J. S. Raza, M. Faheem, M. Guenes. “Industrial wireless sensor and actuator networks in industry 4.0: Exploring requirements, protocols, and challenges — A MAC survey.” WILEY Int J Commun Syst 2019, 2019.

P. Park, S. Coleri Ergen, C. Fischione, C. Lu and K. H. Johansson, “Wireless Network Design for Control Systems: A Survey” IEEE Communications Surveys & Tutorials”, vol. 20, no. 2, 2018.

B. Djukic, S. Valaee, “Link scheduling for Minimum Delay in Spatial Re-use TDMA,” IEEE INFOCOM, Juin 2007.

B. Hajek, G. Sasaki, “Link scheduling in polynomial time,” IEEE Trans. Inform. Theory, vol. 34, no. 5, Septembre 1988.

M. A. Odijk, “Railway timetable generation,” Ph. D., Technische Universiteit Delft, January 1998.

M. R. Garey, D. S. Johnson, “Computers and Intractability : A guide to the Theory of NP-Completeness”, ISBN 0-7167-1044-7, Bell Telephone Laboratories, 1979.

A. D. Gerd Behrmann, K.Larsen, “A tutorial on UPPAAL.”, In Formal Methods for the Design of Real-Time Systems, Volume 3185 of Lecture Notes in Computer Science, 2004.

Rajeev Alur, Costas Courcoubetis, and David L. Dill. Model-checking for real-time systems. In 5th Symposium on Logic in Computer Science (LICS’90), 1990.



  • There are currently no refbacks.

Copyright (c) 2021 ANDRIANANTENAINA Zo Ambinintsoa, RAKOTOMIRAHO Soloniaina, RANDRIAMAROSON Rivo Mahandrisoa

Creative Commons License
This work is licensed under a Creative Commons Attribution 4.0 International License.