Abstract FR:

Dans une application distribuée, les objets peuvent être considérés comme des unités d'exécution. Ce concept existe déjà depuis plusieurs années, cependant une des difficultés consiste à contrôler le fonctionnement d'un objet en tant que composant d'un programme concurrent. La solution que nous avons étudiée consiste à utiliser une approche réactive pour réaliser ce contrôle. Le choix de cette approche est motivé par l'adéquation du modèle réactif au contrôle et à l'utilisation d'une approche formelle. Ce modèle est basé sur la présence d'une entité de contrôle, au sein de chaque objet, que nous avons appelée contrôleur d'exécution réactif. Ceci permet de dissocier ce qui est relatif aux traitements (exécution des méthodes) de ce qui est relatif au contrôle de ces exécutions. En raison de la distribution des objets, nous avons retenu un modèle d'exécution réactif asynchrone permettant de s'affranchir de la contrainte d'une horloge globale à l'ensemble des objets. Nous avons défini pour le contrôleur deux modèles réactifs d'exécution. Le premier modèle dit réactif pur, dans lequel l'activation d'une méthode ne dépend que de l'état d'exécution des autres méthodes, donc de leur ordonnancement. Le contrôleur est représenté par un système de transitions. Le second modèle dit réactif étendu, dans lequel l'activation d'une méthode peut dépendre de la valeur des attributs de l'objet. Nous étendons le modèle réactif pur en utilisant des automates à contraintes. Grâce à une base formelle dans les deux modèles, il est possible d'effectuer des vérifications sur le contrôleur, l'objet ou un groupe d'objets. Nous avons mis en œuvre ce modèle en utilisant des processus légers pour permettre une concurrence inter-méthodes. Le contrôleur est automatiquement compilé à partir d'une spécification. Notre approche permet de vérifier la présence d'interblocages au sein d'un objet ou d'un groupe d'objets. Le code correspondant au contrôleur de l'objet conserve une taille raisonnable.