Abstract FR:

Le theme central de cette these s'articule autour de la verification des qualites des modeles de processus de developpement de logiciels. Son but est de fournir des methodes permettant d'assurer une certaine qualite des modeles en identifiant les types d'inconsistance a detecter et en fournissant les moyens necessaires a leur detection. Ceci nous a amene a nous interesser plus particulierement aux deux points importants que sont la verification de types et la detection d'inconsistances dans les expressions du calcul des predicats du premier ordre. Pour le controle de types, nous proposons un moyen efficace et original de le realiser en utilisant des techniques de programmation sous contraintes. La methode presentee permet d'effectuer ce controle dans des cadres de types relativement complexes. Elle prend en compte les notions de genericite, de surcharge et de coercion. De plus, elle supporte l'introduction de relations d'ordre sur les types (sous-type, heritage de classes. . . ) ainsi que les types fonctions, structures, unions et les differents modes de passage de parametres. . . Pour la detection d'inconsistances dans les expressions du calcul des predicats du premier ordre, nous proposons deux approches distinctes. La premiere concerne la logique du premier ordre restreinte par une contrainte de finitude sur le domaine des interpretations. Nous y montrons son interet, et son adequation aux problemes lies au domaine de la programmation informatique. La seconde approche est relative a la gestion de la semantique predefinie de certains predicats. La methode proposee est fondee sur le principe de resolution du calcul des predicats du premier ordre enrichi de regles de reecriture pour gerer efficacement les predicats predefinis. Ce travail qui se situe dans le cadre des recherches avancees en genie logiciel doit permettre de fournir des aides en vue de simplifier l'activite de modelisation du processus de developpement de logiciel