La composition de spécifications modulaires peut être modélisée, dans le formalisme des catégories, par des colimites de diagrammes. La somme amalgamée permet en particulier d'assembler deux spécifications en précisant les parties communes. Notre travail poursuit cette idée classique selon trois axes. D'un point de vue syntaxique, nous définissons un langage pour représenter les spécifications modulaires construites à partir d'une catégorie de spécifications et de morphismes de spécifications de base. Ce langage est caracterisé formellement par une catégorie de termes finiment cocomplète. D'un point de vue semantique, nous proposons d'associer à tout terme un diagramme. Cette interprétation permet de faire abstraction de certains choix effectués lors de la construction de la spécification modulaire. Pour cela, nous définissons une catégorie de diagrammes ``concrète'', c'est-à-dire dont les flèches peuvent être manipulées effectivement. En considérant le quotient par une certaine congruence, nous obtenons une complétion de la catégorie de base par colimites finies. Nous montrons que le calcul du diagramme associé à un terme définit une équivalence entre la catégorie des termes et la catégorie des diagrammes, ce qui prouve la correction de cette interprétation. Enfin, nous proposons un algorithme pour décider si deux diagrammes sont isomorphes, dans le cas particulier ou la catégorie de base est finie et sans cycle. Cela permet de détecter des isomorphismes ``de construction'' entre spécifications modulaires, c'est-à-dire des isomorphismes qui ne dépendent pas des spécifications de base, mais seulement de la manière dont celles-ci sont assemblées.

Lors de la réalisation des pièces d'un mécanisme, le fabricant se doit de respecter les exigences géométriques exigées par le client. Ces exigences sont issues de besoins fonctionnels du mécanisme à tous les stades de son cycle de vie. Le fabricant lors des opérations successives d'usinage, avec ou sans enlèvement de matière, doit définir les exigences de la géométrie ajoutée au poste. La combinaison de ces exigences affectées de leur tolérance doit être comparée aux exigences géométriques du client. L'objectif du travail présenté est la définition d'une méthode optimisant, rationnellement, les exigences géométriques des surfaces créées. Nous définirons les spécifications géométriques, au sens de l'iso 1101, mais la valeur de ces tolérances ne sera pas abordée dans ce travail, d'autres équipes ayant réalisés des travaux de qualité. L'étude poussée de la méthode 1D utilisée dans l'ensemble du groupe Renault pour définir les fiches schéma nous a montré ses limites lors de la multiplication des posages orientés différemment. Par contre l'optimisation du choix des spécifications influentes a retenu notre intérêt. L'étude des méthodes du bureau d'études pour la recherche de spécifications des pièces composant un mécanisme nous a permis de faire l'analogie avec les phases d'usinages. En effet le passage successif de la pièce sur les différents postes d'usinage s'apparente à des assemblages temporaires qui mettent en œuvre des surfaces actives qu'elles soient de posage ou créées à l'opération. La modélisation du processus d'usinage à l'aide d'une représentation graphique est largement utilisée par la communauté travaillant dans le tolérancement. Nous avons développé dans notre travail un modèle de représentation appelé SPIDER GRAPH. Ce modèle essentiellement pédagogique nous permet de visualiser le déroulement de l'algorithme développé à l'occasion de ce mémoire. Il met en valeur la succession de liens entre les différentes surfaces intervenant pour réaliser une spécification exigée. Deux méthodes utilisant le concept SATT pour la mise en position des ensembles de surfaces de tolérancement de fabrication 3D sont décrites : " Recherche des chemins du process contraignant les degrés de liberté de la spécification fonctionnelle ". Nous avons identifié, en se référant aux résultats développés par DESROCHERS, toutes les combinaisons possibles entre des entités simples et leurs correspondances en termes de type de tolérance. Une validation par un exemple a été établie et un ensemble de spécifications géométriques de fabrication a été généré. Cette méthode qui s'appui successivement sur les surfaces du système de référence ne permet pas une écriture se référant à des systèmes de référence. Nous avons donc développé une alternative à ce travail initial. " Méthode rationnelle de tolérancement de fabrication 3D " Cette méthode est représentée par un logigramme qui prend en compte la hiérarchie des surfaces lors des posages. Il prend également en compte les inversions de spécifications entre la référence et la surface spécifiée. Lors de la création de surfaces temporaires qu'elles soient de posage ou d'usinage, la méthode permet de spécifier ces surfaces dans les opérations considérées. Lors du développement de cette méthode originale, nous avons repris la totalité des fiches de cotations SATT, développées par CLEMENT et aussi les modélisations vectorielles de ces cas d'association décrites par GAUNET. A l'aide des lois d'identification des paramètres de mise en position relative entre SATT, nous avons pu générer, l'ensemble des spécifications géométriques capables de mener au respect de la spécification géométrique fonctionnelle. Cette méthode assure la traçabilité des liens successifs entre les surfaces actives lors des différentes opérations. Ces liens que l'on peut représenter sur le SPIDER GRAPH permettront de déterminer algébriquement ou de façon probabiliste la conséquence de ces différents transferts de pièces entre les poste d'usinage.

La recherche du ou des services de calcul scientifique disponibles sur une grille qui répondent aux besoins d'un utilisateur, aussi appelée courtage de services, est une activité complexe. En effet, les services disponibles sont souvent conçus pour répondre de manière efficace à de nombreux besoins différents. Ceux-ci comportent donc en général de nombreux paramètres et la simple signature du service ne suffit pas pour que l'utilisateur puisse le trouver. La solution proposée dans ces travaux consiste à utiliser une description formelle du domaine d'application comportant l'ensemble des données et des opérateurs du domaine ainsi que les propriétés des opérateurs. Dans le cadre de cette thèse, cette description est effectuée sous la forme d'une spécification algébrique. Un service ou une requête sont alors des termes de l'algèbre associée. En ce qui concerne les signatures, nous combinons le sous-typage des sortes et la surcharge des opérateurs selon le système de type proposé par G. Castagna pour le λ&-calcul. Le courtage consiste alors à effectuer un filtrage modulo la théorie équationnelle associée à la spécification, entre le terme représentant le service souhaité et les termes représentant les services disponibles. Nous proposons et avons implanté deux algorithmes différents inspirés d'un parcours de l'arbre de recherche des solutions contraint par une quantité d'énergie (nombre d'équations et/ou de compositions applicables). Le premier algorithme est directement dérivé des travaux de Gallier et Snyder sur l'unification équationnelle. Nous avons montré sa correction et argumenté sa complétude (ou exhaustivité). Le second algorithme découle d'une définition constructive de l'ensemble des services qui peuvent répondre à la requête d'un utilisateur. L'algorithme consiste alors en un parcours particulier de l'arbre construit pour engendrer le service requis. Nous avons également montré sa correction, et sa complétude pour certaines formes d'équations. Nous illustrons notre approche dans les domaines applicatifs suivants : algèbre linéaire et optimisation, et nous nous intéressons au traitement de la combinaison de domaines applicatifs.

L'espace et le temps sont des concepts indissociables et nécessaires à l'analyse de l'évolution d'entités spatio-temporelles. Modéliser ces évolutions passe par la détection des changements et des relations qui modifient et caractérisent ces entités. Ces changements sont en particulier caractérisés par des modifications liées à la position, à l'empreinte spatiale de ces entités, ou même à leur identité. Une modélisation spatio-temporelle nécessite le développement de solutions de représentation qui permettent d'identifier et d'étudier les processus mis en jeu, leurs causes et leurs conséquences. Le fait que la représentation formelle et informatique d'un phénomène entraîne une description plus ou moins simplifiée de la réalité, implique qu'une telle modélisation retienne le niveau de détail disponible et/ou souhaité de cette description. Idéalement, il devrait être possible d'étudier un phénomène à plusieurs niveaux de granularité dans l'espace et dans le temps. Si de nombreux modèles et approches ont été proposés pour modéliser des évolutions d'entités au sein de phénomènes spatio-temporels, aucun ne permet de disposer d'une structure de représentation permettant de saisir complètement la sémantique de ces applications. Cette recherche propose un modèle de graphe spatio-temporel qui permet de caractériser les principales propriétés de l'évolution d'entités spatiales. Nous distinguons dans ce cadre plusieurs concepts structurants comme les notions d'identité et de relations à travers les dimensions spatiales et temporelles. Pour un temps donné, nous catégorisons les relations spatiales et de filiation et, à travers le temps, les filiations temporelles et les relations spatio-temporelles. Les structures de graphe émergeantes permettent non seulement de caractériser l'évolution d'un ensemble d'entités spatiales, mais aussi de découvrir de nouvelles propriétés. Des fonctions de manipulation de graphe sont développées et appliquées au modèle de graphe spatiotemporel. Ces fonctions identifient des processus génériques ( e.g. vie et mort d'une entité) ou liés à une application spécifique et à sa sémantique. Afin de combiner plusieurs sources d'informations au sein d'un même graphe, des fonctions de jointure permettent l'intégration de plusieurs graphes au sein d'une représentation unifiée. Les propriétés des graphes ainsi constitués et le rôle des différentes entités présentes au sein de ces graphes sont étudiés par une qualification des différents types de routes les reliant. La consistance du modèle de graphe spatio-temporel est abordée à partir d'un algorithme de vérification de contraintes. Nous faisons la différence entre les contraintes de domaine intrinsèques au modèle de graphe, et les contraintes sémantiques dépendantes d'une application en particulier. Une extension de la démarche de modélisation est réalisée à partir d'une structure basée sur les bigraphes qui permet de représenter explicitement un phénomène spatio-temporel selon plusieurs niveaux de granularité spatiale.

Dans le domaine de l'Interaction Homme-Machine, nos travaux concernent l'interaction multiutilisateur et multimodale. Exploitant les avancées importantes en terme de modalités d'interaction, de nombreux collecticiels reposent sur une combinaison de modalités, comme les systèmes multiutilisateurs autour d'une table augmentée. Néanmoins ces systèmes constituent des réalisations ad-hoc en l'absence d'outils de conception. Face à constat, nos contributions conceptuelles et logicielles concernent la phase de spécification de l'interaction multiutilisateur et multimodale. Nous présentons une notation de spécification notée COMM (COllaborative et MultiModale) qui est une extension de CTT par l'introduction de deux concepts, le rôle interactif et la tâche modale, et par la spécialisation des opérateurs temporels, en s'appuyant sur les relations de Allen. La notation COMM est instrumentée par un éditeur logiciel de spécifications COMM, nommé e-COMM ((http://iihm.imag.fr/demo/editeur/). COMM et e-COMM ont été utilisés dans un projet DGA de taille conséquente pour spécifier l'interaction au sein d'un poste de commande de drones militaires.

Cette thèse propose des modèles multi-agents réactifs fondés sur un cadre formel pour la vérification de propriétés et les valider par la simulation et l'expérimentation en considérant la navigation multi-véhicules comme domaine d'application. La navigation multi-véhicules soulève plusieurs problématiques : perception de l'environnement, communication inter-véhicule, évitement d'obstacle, ... Dans ce contexte, nous avons abordé plus particulièrement les aspects suivants : - Concernant la navigation multi-véhicules nous avons abordé deux problèmes spécifiques : la conduite en convoi ou platooning et la navigation autonome. En ce qui concerne la navigation autonome, nous avons mis l'accent sur l'évitement d'obstacles. - Concernant l'approche proposée : nous adoptons les systèmes multi-agents réactifs, dont les interac- tions sont inspirée de la physique. Pour la conduite en convoi, nous proposons un modèle d'interaction basé sur la physique classique. En ce qui concerne l'évitement d'obstacles, nous adoptant un modèle inspiré de la physique statistique. - Nous plaçons les systèmes multi-agents réactifs dans un cadre formel pour la vérification des pro- priétés, compte-tenu des contraintes de sécurité imposées par la classe d'applications cible. Pour faire face à la complexité des modèles, nous proposons une règle et une méthode de vérification compositionnelle. Cela nous a permis de vérifier la satisfaction d'une propriété de sûreté essentielle : la non-collision entre véhicules lors de la conduite en convoi. - Nous abordons également la question de la validation du système multi-agents par la simulation et l'expérimentation : nous avons contribué au développement d'un simulateur de la conduite en convoi et la navigation autonome. Le simulateur prend en compte les caractéristiques physiques des véhicules et est couplé à un outil de visualisation 3D. Nous avons aussi expérimenté nos modèles sur des véhicules tels que le Cycab et le GEM Car.

Une définition des systèmes temps réel est que leur correction dépend de la correction fonctionnelle mais aussi du temps d'exécution des différentes opérations. Les propriétés temps réels sont alors exprimées comme des contraintes temporelles sur les opérations du système. Nous proposons dans cette thèse un autre point de vue où la correction est définie relativement à la validité temporelle des valeurs prises par les variables du système et aux flots de données qui parcourent le système. Pour définir ces conditions de validité, nous nous intéressons au rythme de mise à jour des variables mais aussi aux liens entre les valeurs des différentes variables du système. Une relation dite d'observation est utilisée pour modéliser les communications et les calculs du système qui définissent les liens entre les variables. Un ensemble de relations d'observation modélise l'architecture et les flots de données du système en décrivant les chemins de propagation des valeurs dans le système. Les propriétés temps réels sont alors exprimées comme des contraintes sur ces chemins de propagation permettant d'assurer la validité temporelle des valeurs prises par les variables. La validité temporelle d'une valeur est définie selon la validité temporelle des valeurs des autres variables dont elle dépend et selon le décalage temporel logique ou événementiel introduit par les communications ou les calculs le long des chemins de propagation. Afin de prouver la satisfiabilité d'une spécification définie par une telle architecture et de telles propriétés, nous construisons un système de transitions à état fini bisimilaire à la spécification. L'existence de ce système fini est justifiée par des bornes sur le décalage temporel entre les variables du système. Il est alors possible d'explorer les exécutions définies par ce système de transitions afin de prouver l'existence d'exécutions infinies satisfaisant la spécification.

Dans cette thèse, nous proposons une méthode rigoureuse, formellement fondée pour traiter de l'interopérabilité d'une famille de langages dédiés (DSL) issus d'un même domaine métier. A partir de la sémantique de chacun des DSL, notre démarche construit, par un calcul de co-limite sur des spécifications algébriques, un langage qui unifie les concepts de la famille. L'approche se caractérise notamment par la capacité à traduire automatiquement le code d'un DSL vers le langage unificateur. Un autre bénéfice réside dans la preuve qu'une propriété sur un langage de la famille se décline, par construction, vers l'environnement unifié. La mise en œuvre de la démarche a été outillée ; elle s'appuie principalement sur le logiciel Specware de Kestrel et l'assistant de preuve Isabelle.

Le travail présenté dans cette thèse est une contribution aux méthodes formelles de spécification et de vérification. Les spécifications formelles sont utilisées pour décrire un logiciel, ou plus généralement un système, d'une manière mathématique sans ambiguïté. Des techniques de vérification formelle sont définies sur la base de ces spécifications afin d'assurer l'exactitude d'un système donné. Cependant, les méthodes formelles ne sont souvent pas pratiques et facile à utiliser dans des systèmes réels. L'une des raisons est que de nombreux formalismes de spécification ne sont pas assez riches pour couvrir à la fois les exigences orientées données et orientées comportement. Certains langages de spécification ont été proposés pour couvrir ce genre d'exigences. Le langage Circus se distingue parmi ces langues par une syntaxe et une sémantique riche et complètement intégrées.L'objectif de cette thèse est de fournir un cadre formel pour la spécification et la vérification de systèmes complexes. Les spécifications sont écrites en Circus et la vérification est effectuée soit par des tests ou par des preuves de théorèmes. Des environnements similaires de spécification et de vérification ont déjà été proposés dans la littérature. Une spécificité de notre approche est de combiner des preuves de théorème avec la génération de test. En outre, la plupart des méthodes de génération de tests sont basés sur une caractérisation syntaxique des langages étudiés. Notre environnement est différent car il est basé sur la sémantique dénotationnelle et opérationnelle de Circus. L'assistant de preuves Isabelle/HOL constitue la plateforme formelle au-dessus de laquelle nous avons construit notre environnement de spécification et de vérification.La première contribution principale de notre travail est l'environnement formel de spécification et de preuve Isabelle/Circus, basé sur la sémantique dénotationnelle de Circus. Sur la base d'Isabelle/HOL nous avons fourni une intégration vérifiée d'UTP, la base de la sémantique de Circus. Cette intégration est utilisée pour formaliser la sémantique dénotationnelle du langage Circus. L'environnement Isabelle/Circus associe à cette sémantique des outils de parsing qui aident à écrire des spécifications Circus. Le support de preuve d'Isabelle/HOL peut être utilisé directement pour raisonner sur ces spécifications grâce à la représentation superficielle de la sémantique (shallow embedding). Nous présentons une application de l'environnement à des preuves de raffinement sur des processus Circus (impliquant à la fois des données et des aspects comportementaux).La deuxième contribution est l'environnement de test CirTA construit au-dessus d'Isabelle/Circus. Cet environnement fournit deux tactiques de génération de tests symboliques qui permettent la vérification de deux notions de raffinement: l'inclusion des traces et la réduction de blocages. L'environnement est basé sur une formalisation symbolique de la sémantique opérationnelle de Circus avec Isabelle/Circus. Plusieurs définitions symboliques et tactiques de génération de test sont définies dans le cadre de CirTA. L'infrastructure formelle permet de représenter explicitement les théories de test ainsi que les hypothèses de sélection de test. Des techniques de preuve et de calculs symboliques sont la base des tactiques de génération de test. L'environnement de génération de test a été utilisé dans une étude de cas pour tester un système existant de contrôle de message. Une spécification du système est écrite en Circus, et est utilisé pour générer des tests pour les deux relations de conformité définies pour Circus. Les tests sont ensuite compilés sous forme de méthodes de test JUnit qui sont ensuite exécutées sur une implémentation Java du système étudié.

Au cours du développement embryonnaire, le destin d'une cellule est spécifié par l'expression de gènes dits de lignage. Le contrôle de l'expression de ces gènes est essentiel à la cohérence du développement embryonnaire. Pour savoir comment s'effectue ce contrôle, nous avons choisi un modèle de spécification dans le cerveau postérieur des vertébrés, le rhombencéphale. Au cours de son développement, cet organe comprend sept groupes de cellules homogènes, appelés rhombomères (r) et notés de r1 à r7, qui subissent des processus de spécification distincts. La voie de spécification de r3 et r5 est la mieux connue car elle est contrôlée par un facteur unique, Krox20. En l'absence de ce facteur, les cellules de r3 et r5 ne sont pas correctement spécifiées et voient leur destin neuronal modifié. Dans ce travail de thèse, nous dévoilons les mécanismes qui permettent de contrôler le nombre de cellules exprimant le gène Krox20, donc la taille de r3 et r5. Ces mécanismes contrôlent la dynamique de transcription de Krox20, en régulant l'activité de ses éléments régulateurs. Deux éléments, B et C, sont responsables de l'initiation de l'expression de Krox20 ; un troisième, noté A, l'amplifie et la prolonge grâce à une activité autorégulatrice. Nous montrons (i) que les cellules n'acquièrent l'identité r3/r5 que si elles activent l'élément A, (ii) que l'activation de l'élément A suit un mode tout-ou-rien, selon le niveau d'initiation de Krox20. Ces conclusions ont été obtenues par l'analyse d'un modèle mathématique, contraint par des données expérimentales obtenues chez le poisson-zèbre, et suffisamment résolutif pour décrire l'activation de A à l'échelle moléculaire.