Cette thèse présente une perspective relationnelle à plusieurs aspects de la programmation. L'algèbre relationnelle de Tarski est utilisée pour formuler, et parfois résoudre, des problèmes pertinents à la programmation tels que: la spécification de programmes, l'analyse fonctionnellle de programmes, la vérification de programmes, la conception de programmes et le traitement d'erreurs dans les programmes. La perspective que nous adoptons dans cette thèse est caractérisée par les prémisses suivantes: les programmes sont spécifiés à l'aide de relations; l'analyse fonctionnellle de programmes se fait par composition de fonctions; la conception de programmes se fait par décomposition de relations

Une base de données est au service de plusieurs catégories d'utilisateurs ayant chacune sa vision personnelle et évolutive des différentes sortes d'objets d'un univers. L'application systématique du concept d'abstraction a permis de dégager la notion d'objet pouvant être vu selon différentes facettes, appartenir à plusieurs ensembles et/ou relations, tout en demeurant unique. Ces objets sont spécifiés à l'aide de p-types, concept défini dans le cadre des types abstraits algébriques. La définition d'un p-type est modulaire et évolutive; une vue du p-type est caractérisée par des fonctions attributs et des contraintes d'intégrité. Les contraintes étudiées sont les dépendances entre valeurs d'attributs d'une occurrence d'un p-type (DIA) et les dépendances inter-objets (DIO). L'analyse statique de ces contraintes permet de garantir leur cohérence et de minimiser les vérifications dynamiques

Présentation d'un langage formel pour la spécification des processus communicants. On propose 3 interprétations possibles (modèles) de ce langage: la présentation d'une variété d'algèbres, un système de transition de termes, un arbre (fini ou infini). Introduction d'un calcul pour la construction de réseaux de processus

Réalisation pour l'édition de structures et spécification pou l'édition de la partie fonctionnelle. Le travail présenté se situe dans le domaine de l'aide à la conception des circuits analogiques et digitaux électroniques (projet CASCADE)

Cette thèse porte sur la réalisation d'une maquette du système CESAR, système d'aide à l'analyse d'applications réparties. L'outil réalisé permet de comparer une application décrite par un programme parallèle avec ses spécifications données par un ensemble de formules d'une logique temporelle.

Une methode de conception descendante par affinements successifs de spécifications est présentée. Le point de départ de la conception est la spécification initiale du système sous forme comportementale. L'étape suivante est la specification algorithmique du systeme qui consiste à définir une machine abstraite réalisant le systeme ainsi que la dérivé temporelle admissible sur les entrées et les sorties du système. Ensuite, deux types d'implantation sont proposes: l'implantation fidèle qui est la réalisation d'une machine concrète ayant un comportement semblable à la machine abstraite (à la dérivé temporelle près). Dans le cas contraire, une alarme est envoyée à l'environnement. Cette implantation peut être faite automatiquement grâce à l'interpréteur GRAFCET fidèle. Le deuxième type d'implantation est l'implantation sur ou par construction les contraintes de fonctionnement sont respectées

Le système CESAR proposé dans cette thèse est un système d'aide à la conception des applications reparties. Il permet de décrire l'application étudiée dans un langage algorithmique en termes de processus communiquant par rendez-vous; de spécifier les propriétés de comportement souhaitées au moyen d'une logique temporelle. Le modèle sur lequel ces formules sont analysées est un réseau de Petri interprété généré automatiquement à partir de la description fournie. L'analyse repose sur une évaluation des opérateurs temporels comme points fixes de transformateurs de prédicats sur l'espace d'états du modèle.

Le couplage des approches orientées objets avec la méthode B est une piste pour l'amélioration de l'activité de spécification et de développement de logiciels. La méthode B fournit des notations et des outils supports puissants permettant de modéliser et de vérifier des modèles. Les approches objets fournissent des mécanismes intéressants pour la structuration et le développement de gros systèmes. L'apport de notre travail de thèse contribue aux activités de couplage entre ces deux formalismes en utilisant le prouveur de B pour valider et vérifier des spécifications UML.<br /><br />En étendant les schémas de dérivation d'UML vers B proposés dans des travaux précédents réalisés dans l'équipe de recherche Dédale, nous proposons une approche de dérivation en B de méta-modèles UML, de diagrammes statiques et de diagrammes dynamiques. L'objectif de cette proposition est de vérifier la sémantique et la cohérence entre différents diagrammes de spécifications UML.<br /><br />Notre thèse apporte aussi une contribution au développement de spécifications objets en utilisant la méthode B. La première proposition concerne la prise en compte de certains types d'associations entre classes lors de la dérivation en B. La deuxième proposition concerne la validation de spécifications orientées objets décrites à l'aide de diagrammes de séquence UML2.0.

Les manières de créer et de développer des systèmes informatiques ne cessent d'évoluer. La complexité croissante des logiciels informatiques (répartition du code, utilisation de composants externes, limitation des ressources, etc.) nécessite des méthodes de conception et de validation rigoureuses. Dans ce contexte la phase de test s'avère particulièrement importante car elle contribue à garantir un bon fonctionnement de l'implantation du logiciel, dans son environnement réel d'exécution. Cette thèse définit une méthode automatique de génération de tests destinés à évaluer la robustesse d'une implantation, c'est-à-dire sa capacité à respecter certaines propriétés comportementales malgré un environnement d'exécution dégradé (susceptible de fournir des entrées incorrectes, ou d'inclure des composants externes incapables de rendre le service attendu). L'approche que nous proposons est inspirée des techniques de génération de test utilisées en test de conformité des protocoles de communications dans lesquelles les suites de test sont générées à partir d'un modèle comportementale d'une spécification du logiciel. L'originalité de ce travail consiste à étendre cette technique pour prendre en compte un modèle de fautes (exprimant le comportement dégradé de l'environnement sous forme de mutations syntaxiques de la spécification) et un observateur (exprimant l'ensemble des comportements incorrects du point de vue de la robustesse). Les séquences de test produites sont alors correctes dans le sens où elles ne rejettent que des implantations non robustes vis-à-vis de cet observateur. Un prototype a été réalisé dans le cadre de la boîte à outils IF et évaluée sur des exemples d'implantation Java.

Ce travail aborde le problème de la validation de spécifications de services téléphoniques et notamment la recherche d'interactions entre services. Une interaction correspond à la modification du comportement d'un ou plusieurs services, du fait de la coexistence des services. L'interaction est un obstacle majeur au développement de l'offre de services de télécommunications. La validation de spécifications requiert une modélisation des services et du réseau sous-jacent. Nous proposons une méthode de spécification formelle et de validation de services. Celle-ci est basée sur l'utilisation d'un formalisme synchrone pour la modélisation et la spécification, et sur la mise en oeuvre de méthodes de test pour la validation. Nous avons à cette fin proposé une méthode de test adaptée au problème. Cette méthode a été intégrée à Lutess, un environnement de test fonctionnel de systèmes réactifs synchrones, reposant sur un principe de génération de données dynamique et aléatoire. Elle est basée sur la notion de "guidage par schémas". Un schéma représente une classe de comportements de l'environnement du système sous test, comportements que l'on souhaite tester principalement, soit parce qu'ils sont réalistes, soit parce qu'ils conduisent à une situation estimée critique. Cette méthode a été formalisée, puis validée expérimentalement dans plusieurs études de cas conséquentes, en particulier lors du premier concours de détection d'interaction proposé en marge de la conférence "Feature Interaction Workshop", qui a consacré Lutess "Meilleur outil pour la détection d'interactions".