Cette thèse se situe à l'intersection de deux domaines-clés : l'ingénierie dirigée par les modèles (IDM) et les méthodes formelles, avec différents champs d'application. Elle porte sur la vérification formelle d'applications parallèles modélisées selon l'approche IDM. Dans cette approche, les modèles tiennent un rôle central et permettent de développer une application par transformations successives (automatisées ou non) entre modèles intermédiaires à différents niveaux d'abstraction, jusqu'à la production de code exécutable. Lorsque les modèles ont une sémantique formelle, il est possible d'effectuer une vérification automatisée ou semi-automatisée de l'application. Ces principes sont mis en oeuvre dans TOPCASED, un environnement de développement d'applications critiques embarquées basé sur ECLIPSE, qui permet la vérification formelle par connexion à des boîtes à outils existantes. Cette thèse met en oeuvre l'approche TOPCASED en s'appuyant sur la boîte à outils CADP pour la vérification et sur son plus récent formalisme d'entrée : LOTOS NT. Elle aborde la vérification formelle d'applications IDM à travers deux problèmes concrets : 1) Pour les systèmes GALS (Globalement Asynchrone Localement Synchrone), une méthode de vérification générique par transformation en LOTOS NT est proposée, puis illustrée sur une étude de cas industrielle fournie par AIRBUS : un protocole pour les communications entre un avion et le sol décrit dans le langage synchrone SAM conçu par AIRBUS. 2) Pour les services Web décrits à l'aide de la norme BPEL (Business Process Execution Language), une méthode de vérification est proposée, qui est basée sur une transformation en LOTOS NT des modèles BPEL, en prenant en compte les sous-langages XML Schema, XPath et WSDL sur lesquels repose la norme BPEL.

L'assistance à la conception et plus particulièrement l'assistance à la conception architecturale offre un potentiel riche en applications pour de nombreux thèmes de recherche en informatique. Les travaux présentés dans ce mémoire, concernent plusieurs de ces thèmes. Dans un premier temps, nous présentons le contexte général d'une démarche de conception : l'objet, le processus et les acteurs. Puis, nous nous intéressons à la modélisation des objets en cours de conception et à la prise en compte de leur évolution dans un modèle informatique. Le champ expérimental mis en oeuvre dans cette étude a permis de mettre en évidence les limites des modèles à objets face à la représentation d'objets en cours de conception. En considérant l'approche hypermédia comme un moyen souple d'organisation et de recherche d'informations, adapté au processus de conception, nous présentons une méthode de conception d'hypermédia permettant à l'utilisateur-concepteur d'organiser son domaine de compétences afin de le proposer à d'autres concepteurs. Nous illustrons l'utilisation de cette méthode et mettons en évidence ses limites par la présentation de quelques exemples de mise en oeuvre. Après avoir fait le constat que l'image occupe une place importante dans la conception architecturale, nous proposons différentes utilisations de celle-ci dans l'assistance à la conception : la recherche d'informations techniques par l'image, la veille technologique par l'image et la recherche de références par l'image. Les expérimentations réalisées permettent d'envisagées des extensions quant à la méthode utilisée et aux champs d'investigation considérés.<br />Enfin, afin d'assister certaines activités de conception qui peuvent être collectives, et en considérant la spécificité de l'activité de conception, nous proposons, sous la forme d'un meta-modèle, une représentation du contexte de coopération ainsi qu'une visualisation de ce contexte adaptée à la représentation imagière de l'architecte. Toutes ces approches ont fait l'objet d'applications et d'expérimentations en mettant en oeuvre les dernières technologies de l'information.

Cette thèse se situe à l'intersection de deux domaines-clés : l'ingénierie dirigée par les modèles (IDM) et les méthodes formelles, avec différents champs d'application. Elle porte sur la vérification formelle d'applications parallèles modélisées selon l'approche IDM. Dans cette approche, les modèles tiennent un rôle central et permettent de développer une application par transformations successives (automatisées ou non) entre modèles intermédiaires à différents niveaux d'abstraction, jusqu'à la production de code exécutable. Lorsque les modèles ont une sémantique formelle, il est possible d'effectuer une vérification automatisée ou semi-automatisée de l'application. Ces principes sont mis en oeuvre dans TOPCASED, un environnement de développement d'applications critiques embarquées basé sur ECLIPSE, qui permet la vérification formelle par connexion à des boîtes à outils existantes. Cette thèse met en oeuvre l'approche TOPCASED en s'appuyant sur la boîte à outils CADP pour la vérification et sur son plus récent formalisme d'entrée : LOTOS NT. Elle aborde la vérification formelle d'applications IDM à travers deux problèmes concrets : 1) Pour les systèmes GALS (Globalement Asynchrone Localement Synchrone), une méthode de vérification générique par transformation en LOTOS NT est proposée, puis illustrée sur une étude de cas industrielle fournie par AIRBUS : un protocole pour les communications entre un avion et le sol décrit dans le langage synchrone SAM conçu par AIRBUS. 2) Pour les services Web décrits à l'aide de la norme BPEL (Business Process Execution Language), une méthode de vérification est proposée, qui est basée sur une transformation en LOTOS NT des modèles BPEL, en prenant en compte les sous-langages XML Schema, XPath et WSDL sur lesquels repose la norme BPEL. / The work in this thesis is at the intersection of two major research domains~: Model-Driven Engineering (MDE) and formal methods, and has various fields of application. This thesis deals with the formal verification of parallel applications modelled by the MDE approach. In this approach, models play a central role and enable to develop an application through successive transformations (automated or not) between intermediate models of differing levels of abstraction, until executable code is produced. When models have a formal semantics, the application can be verified, either automatically or semi-automatically. These principles are used in TOPCASED, an ECLIPSE-based development environment for critical embedded applications, which enables formal verification by interconnecting existing tools. This thesis implements the TOPCASED approach by relying on the CADP toolbox for verifying systems, and on its most recent input formalism : LOTOS NT. This thesis tackles the formal verification of MDE applications through two real problems : 1) For GALS (Globally Asynchronous, Locally Synchronous), a generic verification method, based on a transformation to LOTOS NT, is proposed and illustrated by an industrial case-study provided by AIRBUS : a communication protocol between the airplane and the ground described in the synchronous langage SAM designed at AIRBUS. 2) For Web services specified with the BPEL (Business Process Execution Language) norm, a verification method is proposed. It is based on a BPEL to LOTOS NT transformation which takes into account XML Schema, Xpath, and WSDL, the languages on which the BPEL norm is built.