Proving Distributed Algorithms for Mobile Agents: Examples of Spanning Tree Computation in Anonymous Networks
This paper present a framework for describing distributed algorithms for mobile agents in an anonymous network. We make use of the high level encoding of these algorithms as transitions rules. The main advantage of this uniform and formal approach is the
- PDF / 315,954 Bytes
- 6 Pages / 430 x 660 pts Page_size
- 74 Downloads / 232 Views
ct. This paper present a framework for describing distributed algorithms for mobile agents in an anonymous network. We make use of the high level encoding of these algorithms as transitions rules. The main advantage of this uniform and formal approach is the proof correctness of the distributed algorithms. We illustrate this approach by giving examples of distributed computations of a spanning tree by mobile agents in anonymous network. Keywords: mobile agents, spanning tree, distributed algorithms, proofs.
1 1.1
Introduction Background
Nowadays, distributed systems are solicited in potential life services (such as banks, railway stations, airports, trade companies , etc). All of them need reliable applications to propose secure services to their clients. This aim can be realized by proposing powerful models which simplify the design and the proof of distributed algorithms. To formally describe distributed algorithms, several works have tried to propose a ”standard” model for distributed systems. But, unlike sequential algorithms, there is no ”universal” model of computations for the distributed ones. Indeed, designing and proving distributed algorithms is still a hard task and they depend closely on the considered model. The mathematical tool-box provided by local computation model proposed an exciting proof approach for distributed algorithms [1]. Nevertheless, with the success of mobile agent based applications, regards are switched from classical systems (message passing, shared memory, remote procedure call, etc) towards this new paradigm. Mobile agents are programs that can move through a network under their own control and interact with resources and local environments. This technology, S. Rao et al. (Eds.): ICDCN 2008, LNCS 4904, pp. 286–291, 2008. c Springer-Verlag Berlin Heidelberg 2008
Proving Distributed Algorithms for Mobile Agents
287
a profound revolution in computer software technology, is a brand new computing technique promoted for solving a large scale of problems in computer science [2]. Among many others, the distributed computing community is presenting an increasing interest into mobile agents due to their considerable reduction of network load and their overcoming of the network latency . There are also new trends to use this technology in faulty distributed systems for which mobile agents can intuitively give a promoting solution for arising problems. 1.2
Related Works
Stationary process models are the most used computational models for distributed systems. A distributed system is modeled by a graph where the vertices denote processes and the edges denote the communication links between processes. In these models, computational activities are done by concurrent execution of the stationary sequential processes. A panoply of mechanisms exists for interprocess communication. In the message passing mechanism, processes communicate via messages added and removed in a messages-queue. In the shared memory mechanism, processes communicate via global shared variables. In stationary process
Data Loading...
