Abstract FR:

Le suivi et le controle d'une ligne de fabrication d'objets manufactures peut poser des difficultes de controle global a l'operateur de conduite si les objets sont constitues d'elements eclates geographiquement. Dans ce manuscrit, nous proposons un protocole de messagerie industrielle permettant de resoudre ces difficultes de controle global. Dans le chapitre 1, nous decrivons succinctement la norme de messagerie industrielle mms: la partie service ainsi que la partie protocole dont nous nous sommes inspires comme point de depart. De plus, nous presentons les normes d'accompagnement a mms et les propositions normatives de mms sur les bus de terrain fip et profibus. Dans le chapitre 2, nous proposons le protocole multiserveur realisant la transparence pour l'operateur de conduite de la dispersion geographique des elements constitutifs des objets. L'operateur manipule un objet en invoquant des demandes de service vers un serveur particulier comme si l'objet etait monolithique. A charge pour ce serveur de realiser le service de facon repartie. Nous avons developpe et verifie le protocole du modele multiserveur sous forme de systemes de transitions en appliquant une equivalence entre le resultat obtenu par composition des systemes de transitions et sa specification. Dans le chapitre 3, nous etendons notre protocole multiserveur afin qu'il puisse etre capable de confiner un refus d'une demande de service: ce refus pouvant etre du a une defaillance d'un equipement dedie a l'acheminement des donnees ou bien a un echec de realisation d'une application par manque de ressources par exemple. Cette extension a ete realisee en ajoutant une propriete d'atomicite ou de non-atomicite sur les serveurs: un serveur atomique pour un objet donne doit maintenir la coherence de cet objet. Dans le chapitre 4, nous proposons une demarche de verification des protocoles de communication. Cette demarche s'appuie sur le choix du point de vue d'observation des actions circulantes entre entites communicantes et du type d'equivalence a appliquer entre ce que nous observons et ce que nous avons specifie. Nous presentons dans ce meme chapitre le logiciel auto pour ses fonctions d'equivalences ainsi que l'outil developpe au sein de l'equipe: kernext. Dans une annexe, nous introduisons le temps sous forme d'evenements dans un protocole de type client/serveur. Nous proposons un protocole temporise de la couche application comme une extension de la norme mms. Les evenements temporels sont confines au-dessous des machines protocolaires et modelisent des echeances: du client sur reception d'une reponse a un service demande et/ou du serveur sur emission d'une reponse a un service realise. Ce protocole, verifie, est destine a initier le prolongement du travail entrepris vers les protocoles a coherence temporelle