Abstract FR:

Nous nous interessons a l'etude et a la preuve de correction d'algorithmes reactifs et repartis au sein du formalisme unity. Les algorithmes que nous considerons sont supposes s'executer de maniere parallele, c'est-a-dire que plusieurs processus se partagent la realisation des traitements. Nous supposons en outre que le comportement de ces processus est infini dans le temps (reaction) et qu'ils ne partagent ni horloge ni memoire commune (repartition). Ces algorithmes sont decrits dans le langage unity (systemes de transitions equitables) et prouves au sein de la logique associee (logique temporelle lineaire). Dans ce contexte, nous pensons que les assistants de preuve sont necessaires, mais que l'utilisation efficace de demonstrateurs est tributaire d'une modelisation precise, dans le formalisme utilise, des points caracteristiques de la repartition. Nous nous focalisons plus specifiquement sur la communication entre les processus et sur la formalisation de l'etape de mapping sur une architecture repartie. Nous definissons un mecanisme abstrait de communication qui repose sur une relation d'observation. Ce mecanisme, au contraire d'une description explicite d'un echange de messages, permet de prendre en compte les aspects de communication separement des aspects de synchronisation. Nous montrons que cette distinction claire entre les deux notions permet de simplifier la description et la preuve d'algorithmes repartis. Nous definissons egalement un operateur qui represente le mapping d'un programme unity sur une architecture repartie. Cet operateur nous permet de montrer que, malgre la semantique d'entrelacement de unity, le parallelisme reel d'une implantation repartie d'un programme ne remet generalement pas en cause la preuve de correction de ce programme.