21 - STUDENT - Describing and Reasoning about Dynamic Networks Using Concurrent Systems Approach

Yanti Rusmawati (The University of Manchester)

Today computing systems are highly dynamic and complex. They are dynamic in terms of responding to changes. They have to own an ability to evolve as a response to the changes from outside, as well as inside systems without being interrupted. One of such systems are dynamic networks, which have widespread application such as Internet, peer-to-peer networks, mobile networks and wireless networks. Such networks may have links down or nodes move, or routing instability due to change of networks, that make them as unreliable networks. To undertake formal reasoning about such systems, abstract models are essential.
Communication networks are modelled as a collection of n nodes connecting each other through links. Each node communicates by exchanging messages directly or through the intermediate nodes. One usually use a graph, which consists of nodes and edges, to model such networks at high level abstraction. The number of nodes and edges in a dynamic network system may vary over time. For example, a wireless network, which depends heavily on efficient energy consumption, may lose the connection between nodes over time. A node in a mobile network can change its position and its neighbour frequently.
Research about Internet routing instability mainly focuses on route oscillation and convergence problems, as well as duplicate announcement. Research in dynamic network models offers some approaches such as: high-level
models, self-stabilizing systems, geographic models and game theory. Correctness, in dynamic networks, means each node should always know the correct routing information and messages will eventually reach their destination. This research attempts to develop the correctness of dynamic networks in terms of: routing tables are `correct' and routing information is sufficiently correct sufficiently often; message eventually gets delivered; the network is sufficiently connected for sufficiently often; and no persistent livelock. The main contributions of this research are: abstraction of a dynamic network model using concurrent systems approach; factorization of proof ; and run-time verification on implementation of dynamic network models.
We model the dynamic network as a "demonic" process which runs concurrently with routing updates and message passing. This allows us to use temporal logic and fairness constraints to reason about dynamic networks.
We implement the models as multi-threaded programs and use an experimental run-time verification tool to validate them. Future research include stochastic and probabilistic analysis. Furthermore, dynamic networks will be modelled as supervised evolution, where components consist of computational systems which are `monitored' by a supervisory system which may evolve the computation if necessary.

Download file