Ce travail porte sur le problème de la validation des logiciels réactifs synchrones par rapport à des propriétés de sûreté. Les propriétés de sûreté permettent de spécifier les comportements sûrs d'un logiciel. D'une manière générale, notre approche aborde la validation par le test. Dans ce cadre, nous avons défini une technique qui permet de déterminer, à partir des propriétés de sûreté seulement, toutes les données de test favorisant l'observation d'une violation de ces propriétés. Cette technique permet d'anticiper une violation future. Différentes heuristiques ont été implantées pour sélectionner les données de test de façon efficace. Notre proposition a été intégrée à l'outil Lutess. Ce dernier est capable de générer automatiquement et dynamiquement des données de test en s'appuyant sur divers guides. La capacité de nos heuristiques à guider le test vers des situations où la propriété de sûreté peut être violée a été évaluée sur une étude de cas significative proposée par un consortium d'industriels du secteur des télécommunications.

Cette thèse porte sur la construction d'un environnement pour développer des librairies de calcul formel certifié. Nous présentons d'abord les espèces, structures servant à décrire des spécifications par héritage multiple, raffinement et paramétrisation. Les collections, construites par encapsulation d'espèces constituent la librairie utilisateur. Nous définissons également les analyses statiques garantissant la correction d'une définition d'espèce. Ensuite, nous étudions la compilation des espèces et collections vers le langage d'exécution OCAML, en utilisant les objets et modules OCAML. Puis nous détaillons la traduction dans le langage de preuves COQ, la liaison retardée étant traduite par des lambda-abstractions. Nous montrons ensuite comment utiliser cette technique pour optimiser les exécutables OCAML. Enfin, nous prouvons que les analyses faites par le compilateur ainsi que les techniques de traduction sont conforme à la formalisation des espèces faites auparavant en COQ.

Les langages logico-fonctionnels sont des langages de programmation de très haut niveau permettant de définir dans un formalisme unifié des types de données, des fonctions et des prédicats (relations). Plusieurs propositions de langages logico-fonctionnels ont été faites mais toutes se restreignent à des calculs basés sur les termes du premier ordre. Cette restriction permet de programmer avec des types abstraits algébriques mais elle rend difficile la manipulation des structures de données du monde réel, modélisées sous la forme de graphes cycliques. L'objectif de cette thèse est donc d'introduire les graphes cycliques comme structure de données de base des langages logico-fonctionnels. Pour cela, nous voyons les programmes comme des systèmes de réécriture de graphes cycliques et nous étudions les relations de réécriture et de surréduction qu'ils induisent (sémantique opérationnelle). Une propriété importante de la réécriture concerne la confluence : elle exprime le déterminisme des calculs effectués. De nombreux résultats de confluence existent pour la réécriture de termes mais ils ne s'étendent généralement pas aux graphes cycliques. Nous mettons en évidence une classe de graphes cycliques particuliers, les graphes admissibles, pour laquelle nous donnons une preuve de confluence de la réécriture. Concernant la relation de surréduction, nous en proposons une définition puis nous montrons que ce calcul est cohérent et complet par rapport à celui de la réécriture dans le cadre des graphes admissibles. Nous étudions ensuite plusieurs stratégies de réécriture et de surréduction de graphes admissibles, c'est-à-dire des algorithmes permettant d'éliminer des calculs inutiles ou redondants. Nous montrons que nos stratégies sont optimales selon de nombreux critères dépendants des systèmes de réécriture considérés.

L'approche à composants promeut la construction de logiciels à partir de l'assemblage de briques logicielles réutilisables appelées composants. Cette approche ne suppose cependant pas que les fonctionnalités offertes par les composants puissent être disponibles dynamiquement. La disponibilité dynamique fait référence à la situation où des fonctionnalités fournies par des composants qui forment une application deviennent indisponibles ou disponibles de façon continue et en raison de causes diverses, comme le déploiement des composants à l'exécution. Les changements dans les fonctionnalités ont lieu au cours de l'exécution de l'application et sont en dehors de son contrôle. Pour les supporter, une application doit être capable de s'adapter, par exemple en cherchant une fonctionnalité remplaçante ou en incorporant des nouvelle fonctionnalités. Bien que cette situation puisse être supportée dans les modèles à composants actuels, ce support n'est pas explicite et doit être réalisé à travers la programmation. Ceci résulte dans un mélange de logique applicative et de logique d adaptation dédiée à la gestion de la disponibilité dynamique. Ce travail propose un moyen de supporter la disponibilité dynamique dans un modèle à composants à partir d une approche qui introduit d un côté des concepts de l'approche à services dans le modèle à composants et d un autre des concepts permettant à un environnement d exécution, associé au modèle, d'adapter dynamiquement une application à partir d'informations fournies par les composants qui la constituent. Ce travail présente d'abord une étude des approches à composants et à services, et ensuite les concepts et l'implémentation d'un modèle à composants orienté services. Cette implémentation a été évaluée dans un contexte industriel et a été libérée comme un projet de source libre.

Ce travail s'inscrit dans le cadre des méthodes formelles et des outils pour la spécification, la programmation, la vérification et la validation des logiciels réactifs à l'aide du langage synchrone Lustre. Nous avons étendu l'environnement de développement actuel de ces logiciels en lui adjoignant des outils de validation de spécifications et de test de programmes. Nous proposons une technique de construction automatique d'un simulateur aléatoire de l'environnement externe du logiciel ainsi que d'un simulateur des comportements sûrs de ce dernier. Exécutés conjointement, ces deux simulateurs permettent, par observation, la validation des spécifications de l'environnement et des propriétés de sûreté. La simulation de l'environnement constitue également un moyen de test aléatoire du logiciel. Une variante de cette technique est le test des propriétés de sûreté. Ce type de test favorise l'exécution des comportements de l'environnement du logiciel qui peuvent mettre en évidence avec une plus grande probabilité des violations des propriétés de sûreté. Enfin, nous définissons des critères de couverture pour le test structurel en s'appuyant sur le réseau d'opérateurs associé à un programme Lustre. Les conditions d'exécution des composants du réseau satisfaisant les critères sont calculées automatiquement ce qui permet la génération automatique de données de test ainsi que la mesure du taux de couverture obtenu. Toutes ces techniques sont formellement définies. Une illustration de leur application sur un exemple de logiciel synchrone que nous avons développé à cet effet complète notre étude.

Ce travail s'inscrit dans le cadre de la conception d'environnements de test fonctionnel de systèmes réactifs spécifiés formellement en Lustre. Lutess est un tel environnement. Il permet la génération automatique et dynamique de données de test. Cette génération est menée sous contraintes, de manière aléatoire, et éventuellement guidée par des propriétés. Nous avons étendu cet environnement par une méthode de test de type statistique, qui facilite la génération des données de test considérées comme significatives par l'utilisateur. Nous avons validé expérimentalement Lutess avant et après son extension, en montrant que les données générées étaient bien aléatoires et qu'elles respectaient les distributions statistiques attendues. De plus, nous avons utilisé Lutess et la méthode proposée de façon intensive pour la validation de spécifications de services téléphoniques sur deux études de cas conséquentes : une fournie par le CNET et une autre sous la forme d'un concours proposé en marge de la conférence "Feature Interaction Workshop'98". A cette occasion, Lutess a été déclaré "meilleur outil pour la détection d'interactions de services téléphoniques".

Cette thèse s'intéresse à la gestion configurable de la duplication et de la cohérence dans les applications réparties. Elle vise la définition de mécanismes de configuration qui n'impliquent pas de modification du code métier des applications et qui permettent la réutilisation du code de gestion de la duplication et de la cohérence. Le premier objectif permet d'exécuter les applications dans différents environnements sans les réimplémenter. Le deuxième objectif permet de réutiliser les protocoles de duplication et de cohérence dans différents domaines d'application. Cette thèse se place dans le contexte des applications réparties à base de composants. Elle permet la configuration non intrusive de la duplication et de la cohérence en se basant sur la séparation entre le code métier et le code système des composants. Elle permet la réutilisation du code de gestion de la duplication et de la cohérence en modélisant les protocoles en termes de composants qui sont indépendants des applications métier. Les modèles de programmation, de composition et d'exécution proposés sont validés à l'aide d'un prototype Java. Le coût de gestion de la duplication et de la cohérence est évalué et l'applicabilité de l'approche aux environnements CCM et EJB est étudiée. Les capacités de configuration et de réutilisation sont démontrées par des expérimentations avec plusieurs applications et plusieurs protocoles.

En plus de l'utilisation des appareils ubiquitaires qui continue à croître, nous avons accès de plus en plus à d'informations dites contextuelles. Ces informations permettent de connaître l'état de notre environnement et nous aident à prendre les décisions de notre vie quotidienne en fonction du contexte dans lequel nous nous positionnons. Les processus métiers informatiques sont de plus en plus en expansion, alors que les activités qu'ils traitent deviennent automatisées. Toutefois, lorsqu'il s'agit de processus métiers dans un domaine particulier, il y a un manque d'intégration avec ces informations contextuelles. Nous pouvons envisager actuellement une situation donnée dans une partie bien définie du processus à un moment donné et prendre une décision basée sur cette information, mais nous ne pouvons pas contrôler ces informations contextuelles en temps réel et adapter le processus en conséquence, comme nous le faisons dans la vie normale. De plus, la nature statique des processus métiers ne leur permet pas d'être modifiés dynamiquement, les rendant ainsi moins utiles dans un nouveau contexte. Si nous voulons changer le comportement d'un processus métier, nous devons le stopper, le modifier et le redéployer entièrement, ce qui fait perdre toutes les exécutions en cours et l'information associée. Pour répondre à ces problèmes, dans cette thèse, nous présentons le cadre logiciel CEVICHE. Nous proposons une approche qui permet de représenter des processus métiers sensibles au contexte où les informations de contexte sont considérées comme des événements contrôlés en temps réel. Pour cela, nous nous basons sur une nouvelle approche appelée Complex Event Processing (CEP). En utilisant un outil externe pour contrôler le contexte en temps réel, nous sommes alors en mesure de dépasser les limites d'accés à l'information uniquement à des endroits bien précis du processus. Cependant, la connaissance de ces événements ne suffit pas. Nous avons, de plus, besoin d'être capable d'adapter nos processus en conséquence à l'exécution. Avec CEVICHE, nous intégrons les informations obtenues à partir du contexte avec la capacité d'adaptation des processus métiers en cours d'exécution. De plus, l'une des originalités du cadre logiciel CEVICHE vient de la définition d'une opération de désadaptation et de sa mise en œuvre. Défaire l'adaptation peut facilement se passer mal et conduire à des états non désirés et rendre les processus instables. Naïvement considérée comme une tâche triviale, cette question a été peu considérée quand on regarde les approches dynamiques actuelles. Nous proposons donc un modèle formel de ce mécanisme dans CEVICHE. La réalisation du cadre logiciel CEVICHE offre des propriétés de flexibilité et de dynamicité aux processus métiers en se basant sur une approche à composants, permettant ainsi la modification des liaisons en cours d'exécution. En outre, avec CEVICHE, nous apportons une propriété de stabilité au niveau du traitement des événements complexes. Comme toute nouvelle approche, le traitement des événements complexes n'est pas normalisé et est en cours d'évolution, chaque outil utilisant son propre langage pour les exprimer. En définissant notre propre langage, Adaptive Business Process Language (ABPL), comme un langage pivot, CEVICHE facilite l'utilisation de CEP sans les inconvénients de l'adoption anticipée de l'approche. Nous utilisons une technique de type plug-in qui permet aux événements définis en ABPL d'être utilisés dans pratiquement n'importe quel moteur CEP. Cette approche rend les règles de traitement des événements plus faciles à maintenir, car nous centralisons la mise à jour au niveau du plug-in lorsque le langage CEP évolue, ou si nous décidons l'utilisation d'un autre outil, au lieu de mettre à jour toutes les définitions d'événements. Finalement, nous avons validé notre approche en mettant en œuvre un scénario de crise nucléaire, avec des cas d'utilisation qui impliquent de nombreux acteurs, des informations de contexte et des conditions d'adaptation.

This thesis explores the subject of automatic verification of product line models. This approach is based on the hypothesis that to automatically verify product line models, they should first be transformed into a language that makes them computable. In this thesis, product line models are transformed into constraint (logic) programs, then verified against a typology of verification criteria. The typology enumerates, classifies and formalizes a collection of generic verification criteria, i.e. criteria that can be applied (with or without adaptation) to any product line formalism. The typology makes the distinction between two categories of criteria: criteria that deal with the formalism in which models are represented, and the formalism-independent criteria. To identify defects in the first category, the thesis proposes a conformance checking approach directly related with verification of the abstract syntactic aspects of a model. To identify defects in the second category, the thesis proposes a domain-specific verification approach. An optimal algorithm is specified and implemented in constraint logic program for each criterion in the typology. These can be used independently -or in combination- to verify individual product line models. The thesis offers to support the verification of multiple product line models using an integration approach. Besides, this thesis proposes a series of integration strategies that can be used before applying the verification as for individual models. The product line verification approach proposed in this thesis is generic in the sense that it can be reused for any kind of product line model that instantiates the generic meta model based on which it was developed. It is general in the sense that it supports the verification of a comprehensive collection of criteria defined in the typology. This approach was implemented in a prototype tool that supports the specification, transformation, integration, configuration, analysis and verification of product line models via constraints (logic) programming. A benchmark gathering a corpus of 54 product line models was developed, then used in a series of experiments. The experiments showed that (i) the implementation of the domain-specific verification approach is fast and scalable to product line models up-to 2000 artefacts; (ii) the implementation of the conformance checking approach is fast and scalable to product line models up-to 10000 artefacts; and (iii) both approaches are correct and useful for industrial-size models.

La spécification de systèmes complexes est une tâche difficile qui ne peut être accomplie en une seule étape. Dans les méthodes formelles, le concept de raffinement a donné lieu à de nombreux travaux dans lesquels la preuve de la correction entre les différents états de spécifications joue un rôle important. L'activité de refactoring consiste à restructurer un modèle en vue d'améliorer certains facteurs de qualité, tout en préservant la cohérence de ce modèle. Cette thèse préconise l'utilisation de deux techniques de raffinement et de refactoring afin d'établir des modèles UML de qualité c'est-à-dire corrects par construction, extensibles, réutilisables et efficaces. En outre, elle plaide en faveur de l'utilisation conjointe UML (semi-formel) et B, Event-B et CSP (formels). Les principales contributions de cette thèse sont : proposition des patterns de raffinement de diagrammes de classes UML/OCL afin de guider le concepteur lors de la modélisation statique de son application et proposition des schémas de refactoring des modèles UML décrits par des diagrammes de classes, des contraintes OCL et des diagrammes d'états-transitions afin d'aider le concepteur lors de la restructuration des modèles UML.