Spécifications comportementales de composants distribués

L'interface d'un composant logiciel spécifie usuellement le type des messages (ou méthodes) en entrée et en sortie. Dans le cas de composants distribués, il est nécessaire, en plus, de définir des interfaces où les services fournis par un composant peuvent changer au cours du temps, en fonction de son état interne. Il peut être nécessaire par exemple de spécifier un protocole décrivant une séquence de messages échangés entre deux ou plusieurs composants, garantissant l'établissement d'une session, ou d'une clef commune, etc. Le "typage comportemental" s'adresse à ces problèmes, en proposant des systèmes de types plus riches que les types classiques, basés par exemple sur des systèmes d'automates, ou des algèbres de processus. Le but est de pouvoir vérifier qu'un composant est bien typé, et que les interfaces entre les composants d'une configuration sont compatibles.

Le but du stage est l'application de ces principes au cas de la librairie ProActive, qui permet d'une part la programmation d'"objets actifs" distribués et d'un controle fin de leurs comportements, d'autre part la structuration des ces objets sous forme de composants logiciels distribués, dans le cadre du model Fractal

Ce stage pourra éventuellement se prolonger en thèse de doctorat.

Encadrement : 


Laboratoire ou équipe : OASIS (INRIA Sophia Antipolis, UNSA, I3S)
 

Objectifs :  Les développements récents de la librairie ProActive incluent une notion de composants distribués, permettant de créer des composants distribués à partir d'objets actifs, de les assembler, de spécifier leur déploiement, etc. Nous disposons d'autre part d'une sémantique comportementale de ProActive, définissant le modèle comportemental d'un objet actif sous forme de systèmes de transitions. Après une étude bibliographique portant en particulier sur le domaine du typage comportemental, le stagiaire devra proposer un formalisme permettant de spécifier un typage des composants ProActive, et réalisera un prototype permettant de vérifier qu'un composant est compatible avec son type comportemental.

Prérequis : Java, programmation distribuée, méthodes formelles, composants logiciels

Lieu du stage: INRIA  Sophia Antipolis