La recherche dans le domaine des réseaux d'ordinateurs et des agents a
identifié le besoin d'une couche logicielle, permettant de communiquer
de façon uniforme avec des agents fixes et mobiles.  Afin de préserver
la compatibilité avec les infrastructures existantes, nombreuses
solutions proposées utilisent un "home agent", qui "forwarde" les
messages vers les entités mobiles.  Ce mécanisme de "home agent" peut
devenir une contrainte empêchant le passage à l'échelle, en
particulier dans les environnements comme l'"amorphous computer" ou
l'"ubiquitous computing environment".

Libre de toute contrainte de compatibilité, nous avons conçu un
algorithme pour "router" les messages vers des agents mobiles sans
requérir aucune position fixe.  Cet algorithme possède deux
composants: un "directory service" qui maintient une information
distribuée permettant de trouver la position d'un agent mobile et un
"message router" qui utilise cette information pour délivrer des
messages aux agent mobiles.

Dans cet exposé, je décrirai cet algorithme, sa formalisation, ainsi
que sa preuve de correction en Coq.  Deux propriétés furent établies.
La sûreté (safety) garantit que quand un message est délivré il est
délivré au récipient. La vivacité (liveness) établit que les messages
sont finalement délivrés aux agents mobiles. Si le temps le permet, je
parlerai de l'implémentation de cet algorithme dans SoFAR, un système
à agents développé à Southampton (Southampton Framework for Agent
Research).

Page maintenue par Emmanuel Chailloux, dernière modification le 08/12/99 à 18h08

---

PPS

UFR P6