Summary Wireless sensor networks (WSNs) are composed of sensors exchanging the information that they collect from the environment. The use of a scheduler offers an efficient solution to eliminate information redundancy and possible collisions in this network. A scheduler is responsible for choosing the sensors to exchange information at each step of the algorithm's execution. This article presents a WSN handshake algorithm (WSN‐HS) scheduling the communications between every two sensors safely in an exclusive mode. Our WSN‐HS is energy‐efficient. It tries to elaborate communications between sensors with the minimum of messages and thus with the minimum of energy consumption. In addition, our algorithm is fault‐tolerant to sensors' disappearance. Hence, when a sensor runs out of energy, the other sensors in the network will not be blocked and they will continue executing the distributed algorithm. We compare and evaluate our algorithm with another handshake algorithm. The results of the simulation done with two examples of distributed algorithms show that our algorithm significantly minimizes the energy consumption in the WSN. Moreover, in this article, we detail the analysis that emphasizes the efficiency of our WSN‐HS algorithm.

Broadcasting emergency messages has been widely recognized as an important area of research. A crucial issue, in this context, is to ensure the correctness of broadcasting protocols using a formal method to prevent errors before their implementation. In this paper, we propose a new protocol for broadcasting emergency messages in order to inform persons in case of an unexpected situation occurrence. Our protocol consists in applying a clustering mechanism before proceeding with the broadcasting phase. This mechanism is one of the most efficient techniques used in a large-scale network. We formally verify the proposed protocol using the Event-B formal method which supports an incremental development based on the refinement technique.

Vehicular ad-hoc networks (VANETs) technology has become an active research area over the last few years. It has a huge potential to improve traffic efficiency, road safety as well as comfort to both passengers and drivers. In this context, one of the most difficult challenges is to ensure that protocols used in VANETs operate properly as expected and do not cause any inconsistencies. In this paper, we follow the guidelines of systematic literature reviews (SLR) to provide a comparison of the existing approaches formally verifying the correctness of VANETs. We introduce a taxonomy of the proposed solutions and we discuss their goals, limits, verification techniques, etc. We conclude the paper with some research challenges of VANETs that still need to be addressed. So, throughout this present paper, we provide information for researchers and developers to understand the contributions and challenges of the existing studies to pave the way for improving their solution.

Broadcasting official and emergency information is seen as a principle role for controlling crisis situations. In fact, it has a great importance to ensure the communication between network nodes (vehicles, passengers, etc.). This paper presents a survey that examines the existing studies of broadcasting protocols. Our survey follows the guidelines of systematic literature reviews (SLR). It provides a comparison of the existing approaches based on some criteria such as communication technologies and simulation tools. Finally, we highlight some recommendations and possible future researches which need further investigations.

Distributed algorithms have become a rapidly growing field of research due to the advances of the network technologies. However, they are very difficult to implement correctly because they must meet many requirements. In this paper, we follow the guidelines of systematic literature reviews to provide a survey of the existing works ensuring the formal verification of distributed algorithms in static and dynamic networks. Then, we develop a taxonomy of these solutions based on some criteria. Also, a discussion on each criterion is shown with a focus on constraints, requirements and challenges. Finally, we identify some recommendations and open research areas which can motivate the development of more efficient solutions. So, throughout this present paper, we provide information for researchers and developers to understand the contributions and challenges of the existing solutions to pave the way for enhancing their reliability.

The aim of this work is to propose a distributed algorithm, encoded by the local computations model, for computing maximal cliques in dynamic networks.This model provides an abstraction which simplifies the design and the proof of distributed algorithms.To guarantee the correctness of our algorithm, we use the Event-B formal method, which supports a refinement based incremental development using the RODIN platform.

Wireless Sensor Networks (WSNs) are widely used in critical applications (health-care, transport, volcanic eruption monitoring, etc.). Any design error in WSN algorithms can be harmful for the human's life. Therefore, we should be sure that WSN algorithms work correctly from the very first design stages. In this paper, we propose a new approach combining local computations models and refinement to prove correctness of distributed algorithms for WSNs. We use the formal method Event-B to apply refinement. In fact, local computations models provide abstract description of computations which can be easily specified with Event-B. We illustrate our approach by an example of distributed algorithm for WSN.

Dynamic networks are characterized by frequent topology changes due to the unpredictable appearance and disappearance of mobile devices and/or communication links. In this paper, we propose a correct-by-construction approach for proving distributed algorithms in a forest of spanning trees. Our approach consists in two phases. The first one aims to control the dynamic structure of the network by triggering a maintenance operation when the forest is altered. To do so, we develop a formal pattern using the Event-B method which is based on an existing model for building and maintaining a spanning forest in dynamic networks. The second phase of our approach deals with distributed algorithms which can be applied to spanning trees. We illustrate our pattern through an example of a leader election algorithm. The proof statistics show that our solution can save efforts on specifying as well as proving the correctness of distributed algorithms in a forest of spanning trees.

Distributed algorithms are designed to run on interconnected autonomous computing entities for achieving a common task: each entity executes asynchronously the same code and interacts locally with its immediate neighbours. It is widely agreed that the lack of knowledge of the global state makes termination detection one of the most important and complex problems in distributed computing. By relying on refinement, we prove that an algorithm computing a spanning tree with Local Termination Detection (each entity is able to determine only its own termination condition), can be reused and adapted in order to compute the same algorithm with Global Termination Detection (at least one entity is aware that the entire computation is achieved in the network). The main idea relies upon specifying a combination of a well known algorithm namely SSP and the spanning tree algorithm, following a top/down approach. This paper is a starting point towards a general framework for enhancing termination detection property of distributed algorithms and reusing their proofs.

Proving the correctness of distributed algorithms in dynamic networks is a hard task due to the time complexity and the highly dynamic behavior. In the literature, the existing solutions lack a consensus about their developments and their proofs. Moreover, the proofs which have been presented are done manually. In this paper, we propose a reuse based approach for specifying and proving distributed algorithms in dynamic networks. It consists in developing a formal pattern using Event-B method, based on refinement techniques. The proposed pattern allows to handle topological events in dynamic networks and to characterize the concept of time. Our solution relies on evolving graphs as a powerful model to record the evolution of a network topology. To illustrate it, we present an example of a distributed counting algorithm. The proof statistics related to the development of the pattern and the algorithm show the efficiency of our solution.

One of the most important issues in dynamic networks is to prove the correctness of distributed algorithms. This issue has been widely studied in the literature. Nevertheless, we note a lack of consensus about the development and proof of these algorithms. Moreover, the proofs which have been presented are usually done manually. In this paper, we introduce a formal pattern based on evolving graphs which allows to record the dynamic behavior of a network topology. To specify the proposed pattern, we use the Event-B formal method which supports a refinement-based incremental development using RODIN platform.

Due to the lack of knowledge of the global state and the non determinism in the execution of the processes, distributed algorithms are considered to be very complex to design and to prove. However, it becomes crucial to guarantee that these algorithms run as designed. Modularization mechanism in formal development provides a simple way to manage this complexity. In this paper, we rely on the modularization mechanism of the Event-B method and on local computations model to propose a reuse based approach for modelling classes of distributed algorithms. The proposed approach consists in developing a formal pattern defined as a set of proved logical entities called modules. These modules are developed separately and, when needed, can be incorporated and instantiated in a given system development. Such a mechanism can save efforts on modelling and proving the computation steps in distributed algorithms.