Méthodes formelles et à objets pour le développement du logiciel :

Daniel HERMAN Président Jean-Claude DERNIAME Rapporteur Christine CHOPPY Rapporteur Paul LE GUERNIC Examinateur Jean BEZIVIN Examinateur Jean-Claude ROYER ExaminateurFormal methods and object orientation are widely regarded as two fields with significant potential for influence on the future of software engineering. %This thesis focus on the area at the intersection of these fields. We first study this statement by isolating the essential features of the software development. % and stress the qualities required for a good development. %Then we show that each field is an answer to these requirements and they are complementary. The intersection of these two fields is a new and promising domain. We study its issues and synthesize the choices adopted in the current object-oriented formal methodes. In this context, this thesis proposes a software component specification and design method, aimed to facilitate formalization, partially automate the design process and enable control and reuse. The separation between the description levels and the uniformity inside the levels are emphasized first to clarify the design process and second to ensure consistency. Two models are described. The first one, called the graphic abstract type model, defines the components through a dynamic and a functional aspect. The dynamic modelling is natural for objects and expressed through guarded finite state machines. Beyond its accessiblility to non-expert users, the main interest of the dynamic model is to support the construction of the algebraic specifications, which constitutes the functional axis. The second model, called the formal class model, is a general, formal and abstract model for object oriented design. Based on algebraic data types, it permits abstract reasoning and the implementation in several object oriented programming languages. The proposed model are independent and adaptable in other development methods. We propose a transition methods between these models, that enhances specification control and reuse. Several writing and proof tools are common to both models. It has also been kept in mind to open our system to other specification environments.Les spécifications formelles et la modélisation par objets sont considérés comme deux champs ayant un fort potentiel d'influence sur l'avenir du génie logiciel. Dans un premier temps, nous étudions cette affirmation en dégageant les caractéristiques essentielles du développement du logiciel. L'intersection des deux champs est un domaine nouveau et prometteur. Nous en étudions les différents variantes et nous synthétisons les choix faits dans les méthodes formelles à objets actuelles. Dans ce contexte, cette thèse propose une méthode de spécification et de conception de composants logiciels destinée à faciliter la formalisation, automatiser partiellement le processus de conception, permettre le contrôle et la réutilisation des classes avant implantation. L'accent est mis sur la séparation entre les niveaux de description pour clarifier le processus de conception et sur l'uniformisation à l'intérieur des niveaux de description pour assurer la cohérence. Deux modèles sont décrits. Le premier modèle, dit des types abstraits graphiques, définit les composants suivant un axe dynamique et suivant un axe fonctionnel. La modélisation dynamique, naturelle pour des objets est donnée en termes d'automates d'états finis gardés. Outre sa lisibilité, le modèle dynamique a pour intérêt majeur la construction guidée de spécifications algébriques, support de l'axe fonctionnel. Le second modèle, dit des classes formelles, est un modèle général, formel et abstrait pour la conception à objets. Basé sur les types abstraits algébriques, il permet le raisonnement abstrait et ma mise en oeuvre dans différents langages de programmation à objets. Les modèles présentés sont indépendants et sont adaptables dans d'autres méthodes de développement. Nous proposons une méthode de transition entre ces deux modèles, qui favorise le contrôle et la réutilisation des spécifications. Plusieurs outils d'écriture et de preuve sont communs aux deux modèles et nous insistons sur l'ouverture vers d'autres environnements de spécification