Abstract FR:

Cette thèse traite d'une construction linguistique, le module contrôle par priorité (en abrégé mcp) destinée à représenter les objets partages par des processus dans un environnement de parallélisme. Le mcp est un constructeur de types abstraits dote d'un contrôleur local appelé synchroniseur. Le synchroniseur a été conçu selon l'idée qu'il existe deux sortes de contrôles pour accéder a un objet partage: les contrôles lies a l'état intrinseque de l'objet et ceux définis par ordonnancement. Ces deux types de contrôle sont sépares dans un mcp, une notion de priorité globale permettant d'exprimer avec concision l'ordonnancement des opérations. Deux implantations sont présentées dans la thèse: l'une validée en terme de sémaphores destinée a un monoprocesseur, l'autre utilisant un langage d'acteurs visant des environnements distribues. La suite de ce travail concerne deux approches de la validation de solutions utilisant des mcp. Dans la première approche, une sémantique du synchroniseur a été définie dans une logique temporelle linéaire. Le système de preuve offre au programmeur des spécifications en logique temporelle utilisant des constructions du synchroniseur; ces spécifications sont des conditions suffisantes pour garantir des propriétés relatives à l'état intrinseque de l'objet ou à un ordonnancement. Dans la seconde approche, le mcp est modélisé au moyen de machines abstraites. Une machine abstraite est un système de transitions incluant des variations et des messages dont les transitions sont régies par des affectations vectorielles gardées appelées actions. La sémantique d'un synchroniseur est obtenue comme la solution d'un système d'équations au point fixe sur les actions. Les preuves utilisent la même démarche