Ce travail analyse les problèmes posés par l'administration des systèmes répartis. Il dégage un ensemble de services de base permettant la construction d'un ensemble complet de services d'administration. Il définit donc un noyau d'administration constitué d'un service étendue de gestion de la configuration, remplissant à la fois la spécification de la configuration, la gestion des modifications, et la gestion de l'audit. La spécification de la configuration permet de fournir une description de haut niveau des ressources du système. Cette spécification est décrite grâce à une extension du langage C++. L'extension est réalisée grâce à une bibliothèque de classes et un préprocesseur permettant la spécification des relations entre les différentes entités et celle des notifications qui pourront être émises pour signaler un changement de l'état d'une ressource. Nous proposons un protocole original de gestion des modifications de la configuration. Il permet au système d'accepter les changements structurels (retrait, ajout, connexion et déconnexion). L'algorithme proposé permet au système d'évoluer d'une configuration vers une autre sans mettre en cause la cohérence des applications qui s'exécutent sur le système, et ceci avec un coût très bas en terme de ralentissement observé

Ce mémoire présente l'étude d'une approche particulière des langages de programmation logico-fonctionnels, fondée sur la logique des clauses de Horn avec égalité. Nous définissons d'abord la syntaxe et la sémantique des programmes que nous considérons. La syntaxe est celle de la logique des clauses de Horn avec égalité. La sémantique est donnée par le plus petit e-modele de Herbrand associe a un programme. Nous nous intéressons ensuite au calcul dans ce langage. Nous proposons pour cela une nouvelle règle appelée sldei-resolution comme seule règle de calcul. Nous montrons sa cohérence, sa complétude ainsi que sa completude forte. La mise en œuvre de la règle sldei-resolution nécessite un algorithme de resolution d'équations. Nous étudions de tels algorithmes fondes sur la relation de surreduction, et améliorons ces algorithmes par l'utilisation de stratégies de surreduction. Cependant, ces stratégies ne sont pas complètes dans le cas général. Nous proposons alors des conditions suffisantes sur ces stratégies afin de préserver la complétude des algorithmes considérés. Nous caractérisons ensuite une classe de programmes, dits uniformes, pour lesquels l'utilisation de n'importe quelle stratégie de surreduction donne un algorithme complet de resolution d'équations. Nous donnons de plus une methode de vérification de l'uniformité d'un programme. Par ailleurs, nous proposons des conditions syntaxiques pour qu'un programme soit uniforme. Enfin, nous décrivons les principaux traits d'un langage de programmation fonde sur l'approche présentée dans ce mémoire, et l'implantation que nous avons réalisée

La spécification par type abstrait algébrique permet de décrire le comportement de structures de données particulières telles que les files, piles, arbres, etc. D'autre part, la généricité permet de spécifier le comportement de classes de structures. Nous nous intéressons dans cet ouvrage aux types abstraits génériques exprimes dans le formalisme algébrique. Ces spécifications génériques sont souvent liées entre elles par des relations telles que l'importation, la paramétrisation, etc. Toute instance d'une spécification générique s1, paramétrée par une spécification s2, doit vérifier des conditions décrites formellement dans s2. En général, ce type de vérification se traduit par la démonstration de formules logiques dans une théorie particulière. Nous définissons les différentes relations sémantiques qu'il faut valider dans le cadre d'un langage de programmation générique. Nous montrons également les principales caractéristiques de notre implémentation. Celle-ci aide a réaliser les validations sémantiques en utilisant un démonstrateur semi-automatique de théorèmes. Les expériences réalisées avec notre implantation nous ont conduit a constater le besoin de la réutilisation de démonstrations. Aussi avons nous propose les fonctionnalités d'un atelier de démonstration en utilisant le formalisme algébrique

Présentation de quelques rappels sur les grammaires statiques. Il est aussi montre la nécessité du recours a des techniques issues du génie logiciel pour arriver à une réelle ingénierie du logiciel. Présentation d'un inventaire des besoins en génie logiciel pour la construction de systèmes de traduction assistée par ordinateur (tao). Présentation d'un prototype de poste de travail linguistique adapte a la construction de grammaires statiques et déjà teste par quelques utilisateurs pilotes

Nous proposons une approche où la phase d'analyse est remplacée par une phase d'édition dirigée par la grammaire du langage naturel à traduire. Nous spécifions un système où l'interaction est faite avec l'auteur du texte. En cas de faute, une reformulation correcte est proposée; en cas d'ambiguïté, les différentes interprétations sont paraphrasées. Pour réaliser l'analyseur, nous avons défini une version interprétable du Langage de Spécification de Correspodances Structurales utilisé au GETA pour décrire des langages naturels et les descripteurs abstraits correspondants. Nous avons implémenté une maquette de l'interpréteur

Dans cette thèse, on présente un cadre qui associe la spécification algèbrique de types à l'algèbre de programme. La principale caractéristique de cette approche est fournie par les opérateurs génériques définissables par les utilisateurs qui donnent une grande puissance d'expression aux règles d'équivalence. En particulier, la structure de certains types est contenue implicitement dans des opérateurs génériques comme l'homomorphisme et l'homomorphisme «inverse». Les applications de cette algèbre de programmes typés incluent la preuve de programmes sans induction explicite, et les méthodes de transformation de programmes comme le «folding-unfolding»

Dans le cadre du projet OPALE, ayant pour objectif la conception d'une machine base de connaissance PROLOG, on spécifie un opérateur devant réaliser l'unification au vol sur un flux de données issu d'une unité de disque. Pour améliorer les performances de l'interprétation de PROLOG dans un contexte base de connaissances, cet opérateur doit unifier non pas un mais un ensemble de buts ce, en accord avec la stratégie de recherche élaborée. On propose de décomposer l'unification en une étape de préunification suivie d'une étape d'association. Les algorithmes sont alors validés et intégrés en une maquette logicielle. Nous abordons l'aspect matériel en proposant une méthodologie de conception s'appuyant sur des notions développées dans la programmation orientée objet. Puis nous amorçons la réalisation du «circuit» à l'aide d'un compilateur de silicium

Étude d'un modèle mathématique pour formaliser le comportement des systèmes parallèles et temps réel, à des fins de spécification de problèmes, de description, d'analyse et de preuve de réalisations. Construction, à partir des mêmes notions, d'un calcul formel conduisant à des méthodes systématiques d'analyse de systèmes logiques temporisés, au niveau algorithmique

Cette thèse propose un environnement pour la spécification et l'analyse des processus parallèles communicants et décrit en détail la partie de cet environnement qui permet de spécifier chaque processus et de construire des réseaux de processus. Un langage permet de décrire l'activité de communication de chaque processus et des opérateurs décrivent les constructions de réseaux. De plus, toute description de processus ou de réseau peut être rangée dans une base de données et associées à une représentation graphique. Cette représentation peut être utilisée pour construire des réseaux et de telles constructions sont traduites sous forme d'expression utilisant les opérateurs de construction. Enfin, le calcul du processus résultant d'une construction est présenté et un algorithme d'optimisation est proposé

Sur la base d'un modèle des fonctions essentielles requises pour l'écriture d'un didacticiel, nous étudions les problèmes posés par la spécification de ces fonctions et leur programmation informatique. Les méthodes proposées sont issues d'une expérience concrète et réussie de production de didacticiels de taille importante. De plus nous rendons compte sur le plan génie logiciel, et nous décrivons l'ensemble des outils que nous avons du spécifier et réaliser pour favoriser la production de didacticiels fiables, portables et modifiables.