Modelling and parameterized verification of mobile networks

Parameterized verification. Parameterized models provide a powerful way of modelling and reasoning about complex systems made of arbitrarily many copies of a single component. The aim of parameterized verification is then to check properties of all instances of the model at once (i.e., for any number of copies of the component). Distributed protocols, and specifically protocols running on ad hoc networks are a motivating example for this setting, as the correctness of the protocol should not depend on the exact number of participants. Other applications include multi-threaded programmes, distributed algorithms, and different families of biological of chemical systems. For these parameterized systems, several models and verification algorithms were proposed in the literature, mainly depending on the application: population protocols, threshold automata, broadcast procotols, etc.

Mobile networks. For systems such as mobile ad hoc networks, or even chemical species in a solution, the model of the system should incorporate the inherent mobility of the components of the network. In the literature on the verification of mobile ad hoc networks, the usual assumption is that the network topology evolves non-deterministically, abstracting away the physical constraints in the movement of nodes. Moreover, when node or communication failures are considered, these events are non-deterministic alternatives to the perfect behaviour (in which nodes and communications are reliable). As a consequence, between two message broadcasts, arbitrary changes in the communication topology or in the set of alive nodes may occur during the reconfiguration step. Such arbitrary reconfigurations may not be realistic, especially in settings where communications are frequent enough, and mobility is relatively slow and not chaotic. As an example, a device may enter and exit the communication range of a transmitter while exchanging synchronisation messages at a very high rate. From a theoretical perspective, arbitrary topology changes are very appealing since they transform the semantics into behaviours of a well-structured transition system, and thus enable the verification of basic properties. However, a realistic model for communication protocols on mobile ad hoc networks is lacking. Population protocols, from the distributed algorithm community can be used to represent interactions of chemical species. Usually, interaction between the molecules are arbitrary: any pair of molecule present in the solution can “meet” to generate products from their reaction. The distance between species and the position in the solution is not considered. Here also, the mobility of molecules should be reflected in a realistic model.

Objectives. The first objective of is to design a model that faithfully represents mobility in ad hoc networks, and similarly mobility in solutions with chemical reactants. It should reflect on the one hand, the placement of nodes/molecules at a given time instant, and on the other hand, the physical movement of nodes/molecules over time. Current graph-based models for the communication topology fall short at these objectives. The second objective will be to develop verification algorithms for the proposed models.