Abstract FR:

Les specifications formelles et la modelisation par objets sont consideres comme deux champs ayant un fort potentiel d'influence sur l'avenir du genie logiciel. Dans un premier temps, nous etudions cette affirmation en degageant les caracteristiques essentielles du developpement du logiciel. L'intersection des deux champs est un domaine nouveau et prometteur. Nous en etudions les differents variantes et nous synthetisons les choix faits dans les methodes formelles a objets actuelles. Dans ce contexte, cette these propose une methode de specification et de conception de composants logiciels destinee a faciliter la formalisation, automatiser partiellement le processus de conception, permettre le controle et la reutilisation des classes avant implantation. L'accent est mis sur la separation entre les niveaux de description pour clarifier le processus de conception et sur l'uniformisation a l'interieur des niveaux de description pour assurer la coherence. Deux modeles sont decrits. Le premier modele, dit des types abstraits graphiques, definit les composants suivant un axe dynamique et suivant un axe fonctionnel. La modelisation dynamique, naturelle pour des objets est donnee en termes d'automates d'etats finis gardes. Outre sa lisibilite, le modele dynamique a pour interet majeur la construction guidee de specifications algebriques, support de l'axe fonctionnel. Le second modele, dit des classes formelles, est un modele general, formel et abstrait pour la conception a objets. Base sur les types abstraits algebriques, il permet le raisonnement abstrait et ma mise en uvre dans differents langages de programmation a objets. Les modeles presentes sont independants et sont adaptables dans d'autres methodes de developpement. Nous proposons une methode de transition entre ces deux modeles, qui favorise le controle et la reutilisation des specifications. Plusieurs outils d'ecriture et de preuve sont communs aux deux modeles et nous insistons sur l'ouverture vers d'autres environnements de specification