L'objectif de cette thèse est d'explorer des descriptions formelles pour la structure et le fonctionnement des systèmes biologiques, ainsi que des outils formels pour raisonner au sujet de leur comportement. Cette thèse s'inscrit dans les travaux étudiant les modèles informatiques sûrs où les calculs sont exprimés par l'intermédiaire de la réécriture, et où nous pouvons compter sur la vérification formelle pour exprimer et valider les propriétés des modèles. Dans cette thèse nous développons un calcul de réécriture d'ordre supérieur pour décrire des molécules, des règles de réaction, et la génération des réseaux biochimiques. Le calcul est basé sur la métaphore chimique en décrivant les calculs en termes de solutions chimiques dans lesquelles les molécules représentant des données agissent l'une sur l'autre librement selon des règles de réaction. Ainsi nous avons obtenu un Calcul Biochimique Abstrait étendant le modèle chimique d'ordre supérieur en considérant des molécules structurées. Le calcul est équipé d'une spécification naturelle de la concurrence et des mécanismes de contrôle grâce à l'expression des stratégies de réécriture sous forme de molécules. La description des complexes moléculaires ou des réactifs chimiques appartient à une classe spécifique de graphes. Nous définissons la structure des graphes avec ports et nous montrons que les principes du calcul biochimique instanciés pour les graphes avec ports sont assez expressifs pour modéliser des systèmes autonomes et des réseaux biochimiques. En plus, les techniques de la réécriture stratégique ouvrent la voie au raisonnement basé sur les calculs et à la vérification des propriétés des systèmes modélisés.

Cette these contribue a l'etude des semantiques pour la specification et la verification des systemes reactifs. Plus precisement, nous comparons des semantiques comportementales, basees sur la bisimulation avec celles induites par des logiques modales du temps arborescent. Dans la premiere partie, nous considerons les modeles d'entrelacement pour les systemes sequentiels non-deterministes. Plusieurs travaux recents ont montre que dans le cadre des systemes a branchement infini (c-a-d. non-determinisme infini), l'equivalence de bisimulation (forte), reconnue comme l'equivalence semantique de base pour le temps arborescent, est strictement plus fine que celles induites par les logiques du temps arborescent (nous savons depuis longtemps qu'elles coincident sous l'hypothese de branchement fini). Nous utilisons les Processus Ordinaux de Klop, et, en derivant une notion de pouvoir de distinction d'une equivalence semantique, nous montrons dans un cadre parfaitement unifie que la bisimulation est plus fine que les logiques du temps arborescent, mais aussi que pour une large classe de combinateurs, les congruences engendrees par les logiques restent strictement plus faibles que la bisimulation. Dans la deuxieme partie de la these, nous considerons les modeles d'ordre partiel pour les systemes paralleles, dans lesquels on dispose d'une definition satisfaisante de l'operation de raffinement de programme (cette notion est liee a la methode classique de conception hierarchique des programmes). Parmi les equivalences semantiques de la litterature, la history preserving bisimulation est particulierement interessante car c'est une congruence pour l'operation de raffinement quand les systemes n'ont pas d'action invisible. En utilisant une caracterisation de cette equivalence en termes d'une bisimulation avant-arriere, nous exhibons deux caracterisations logiques, ainsi qu'un algorithme de traduction entre ces deux logiques. Nous etudions aussi plusieurs variantes de cette bisimulation avant-arriere. Enfin, nous elargissons le champ de travail en considerant les modeles d'ordre partiel avec actions invisibles. Nous montrons que la bisimulation avant-arriere susmentionnee, adaptee a ce cadre, coincide avec la branching bisimulation sur les arbres causaux, mais aussi avec deux nouvelles equivalences~: l'equivalence de mixed-ordering branching et la history preserving branching bisimulation, que nous etudions.

Nous étudions la mise en œuvre du rendez-vous multiprocessus et de l'équité dans les langages du type csp généralise. Nous proposons une methode de construction des protocoles. Cette methode consiste a mettre en œuvre ces protocoles a partir d'un schéma de protocole, c'est-a-dire un protocole comportant des parties abstraites. La mise en œuvre effective d'un protocole se fait en remplaçant les parties abstraites par du code. Nous discutons le choix de ce code a l'aide d'exemples tires de la littérature. Nous étudions six notions d'équité dites classiques. Nous montrons que parmi ces six notions d'équité seules les notions d'équité dites fortes accroissent la vivacité. Nous montrons aussi qu'en général il est impossible de construire un protocole réalisant une de ces notions d'équité fortes: seule la strong process fairness peut l'être, et cela seulement lorsque le rendez-vous est binaire. Nous etudions la construction des protocoles réalisant la weak interaction fairness et la strong process fairness (avec rendez-vous binaire). Nous dérivons, a partir d'une spécification, un schéma pour chacune de ces notions d'équité

L'objectif principal de cette thèse est l'étude et la formalisation de nouvelles constructions permettant d'augmenter l'expressivité du filtrage et des langages à base de règles en général. Ceci est motivé par le développement de Tom, un système qui enrichit les langages impératifs comme Java et C avec des constructions de haut niveau comme le filtrage et les stratégies. Une première extension que l'on propose est la notion d'anti-patterns, i.e. des motifs qui peuvent contenir des symboles de complément. La négation est intrinsèque au raisonnement habituel, et la plupart du temps quand on cherche quelque chose, on base nos motifs sur des conditions positives et négatives. Cela doit naturellement se retrouver dans les logiciels permettant les recherches à base de motifs. Par exemple, les anti-patterns permettent de spécifier qu'on cherche des voitures blanches qui ne sont pas des monospaces, ou qu'on cherche une liste d'objets qui ne contient pas deux éléments identiques. Nous définissons alors de manière formelle la sémantique des anti-patterns dans le cas syntaxique, i.e. quand les symboles n'ont aucune théorie associée, et aussi modulo une théorie équationnelle arbitraire. Puis nous étendons la notion classique de filtrage entre les motifs et les termes clos au filtrage entre les anti-patterns et les termes clos (anti-filtrage). S'inspirant de l'expressivité des règles de production, nous proposons plusieurs extensions aux constructions de filtrage fournies par Tom. Par conséquent, la condition pour l'application d'une règle n'est plus une simple contrainte de filtrage, mais une combinaison (conjonction ou disjonction) de contraintes de filtrage et d'anti-filtrage ainsi que d'autres types de conditions. Les techniques classiques de compilation du filtrage ne sont pas bien adaptées à ces conditions complexes. Ceci a motivé l'étude d'une nouvelle méthode de compilation basée sur des systèmes de réécriture. L'application de ces systèmes est contrôlée par des stratégies, permettant la mise en place d'extensions futures (comme la prise en compte de nouvelles théories de filtrage) de manière simple et naturelle, sans interférer avec le code existant. Nous avons complètement réécrit le compilateur de Tom en utilisant cette technique. Une fois tous ces éléments rassemblés, on obtient un environnement pour décrire et implémenter des transformations de manière élégante et concise. Pour promouvoir son utilisation dans des projets complexes du milieu industriel, nous développons une technique pour extraire de manière automatique des informations structurelles à partir d'une hiérarchie arbitraire de classes Java. Cela permet l'intégration du filtrage offert par Tom dans n'importe quelle application Java, nouvelle ou déjà existante.

Cette dernière décennie a vu apparaître et se développer toute une théorie sur l'échantillonnage des surfaces lisses. L'objectif était de trouver des conditions d'échantillonnage qui assurent une bonne reconstruction d'une surface lisse S à partir d'un sous-ensemble fini E de points de S. Parmi ces conditions, l'une des plus importantes est sans conteste la condition d'e-échantillonnage, introduite par Amenta et Bern, qui stipule que tout point p de S doit être à distance de E au plus e fois lfs(p), où lfs(p) désigne la distance de p à l'axe médian de S. Amenta et Bern ont montré qu'il est possible d'extraire de la triangulation de Delaunay d'un e-échantillon E une surface affine par morceaux qui approxime S du point de vue topologique (isotopie) et géométrique (distance de Hausdorff). Néanmoins restaient ouvertes les questions cruciales de pouvoir vérifier si un ensemble de points donné est un e-échantillon d'une part, et de construire des e-échantillons d'une surface lisse donnée d'autre part. De plus, les conditions d'échantillonnage proposées jusque là n'offraient des garanties que dans le cas lisse, puisque lfs s'annule aux points où la surface n'est pas différentiable. Dans cette thèse, nous introduisons le concept d'e-échantillon lâche, qui peut être vu comme une version faible de la notion d'e-échantillon. L'avantage majeur des e-échantillons lâches sur les e-échantillons classiques est qu'ils sont plus faciles à vérifier et à construire. Plus précisément, vérifier si un ensemble fini de points est un e-échantillon lâche revient à regarder si les rayons d'un nombre fini de boules sont suffisamment petits. Quand la surface S est lisse, nous montrons que les e-échantillons sont des e-échantillons lâches et réciproquement, à condition que e soit suffisamment petit. Il s'ensuit que les e-échantillons lâches offrent les mêmes garanties topologiques et géométriques que les e-échantillons. Nous étendons ensuite nos résultats au cas où la surface échantillonnée est non lisse en introduisant une nouvelle grandeur, appelée rayon Lipschitzien, qui joue un rôle similaire à lfs dans le cas lisse, mais qui s'avère être bien défini et positif sur une plus large classe d'objets. Plus précisément, il caractérise la classe des surfaces Lipschitziennes, qui inclut entre autres toutes les surfaces lisses par morceaux pour lesquelles la variation des normales aux abords des points singuliers n'est pas trop forte. Notre résultat principal est que, si S est une surface Lipschitzienne et E un ensemble fini de points de S tel que tout point de S est à distance de E au plus une fraction du rayon Lipschitzien de S, alors nous obtenons le même type de garanties que dans le cas lisse, à savoir : la triangulation de Delaunay de E restreinte à S est une variété isotope à S et à distance de Hausdorff O(e) de S, à condition que ses facettes ne soient pas trop aplaties. Nous étendons également ce résultat aux échantillons lâches. Enfin, nous donnons des bornes optimales sur la taille de ces échantillons. Afin de montrer l'intérêt pratique des échantillons lâches, nous présentons ensuite un algorithme très simple capable de construire des maillages certifiés de surfaces. Etant donné une surface S compacte, Lipschitzienne et sans bord, et un paramètre positif e, l'algorithme génère un e-échantillon lâche E de S de taille optimale, ainsi qu'un maillage triangulaire extrait de la triangulation de Delaunay de E. Grâce à nos résultats théoriques, nous pouvons garantir que ce maillage triangulaire est une bonne approximation de S, tant sur le plan topologique que géométrique, et ce sous des hypothèses raisonnables sur le paramètre d'entrée e. Un aspect remarquable de l'algorithme est que S n'a besoin d'être connue qu'à travers un oracle capable de détecter les points d'intersection de n'importe quel segment avec la surface. Ceci rend l'algorithme assez générique pour être utilisé dans de nombreux contextes pratiques et sur une large gamme de surfaces. Nous illustrons cette généricité à travers une série d'applications : maillage de surfaces implicites, remaillage de polyèdres, sondage de surfaces inconnues, maillage de volumes.

Dans cette thèse, nous nous intéressons à la spécification et à l'analyse modulaires de politiques de sécurité flexibles basées sur des règles.<br />Nous introduisons l'utilisation du formalisme de réécriture stratégique dans ce domaine, afin que notre cadre hérite des techniques, des théorèmes, et des outils de la théorie de réécriture. Ceci nous permet d'énoncer facilement et de vérifier des propriétés importantes des politiques de sécurité telles que l'absence des conflits.<br />En outre, nous développons des méthodes basées sur la réécriture de termes pour vérifier des propriétés plus élaborées des politiques. Ces propriétés sont la sûreté dans le contrôle d'accès et la détection des flux d'information dans des politiques obligatoires.<br />Par ailleurs, nous montrons que les stratégies de réécriture sont importantes pour préserver des propriétés des politiques par composition. Les langages de stratégies disponibles dans des systèmes comme Tom, Stratego, Maude, ASF+SDF et Elan, nous permettent de définir plusieurs genres de combinateurs de politiques.<br />Enfin, nous fournissons également une méthodologie pour imposer à des applications existantes, de respecter des politiques basées sur la réécriture via la programmation par aspects. Les politiques sont tissées dans le code existant, ce qui génère des programmes mettant en oeuvre des moniteurs de référence. La réutilisation des politiques et des programmes est améliorée car ils peuvent être maintenus indépendamment.

La conception des systèmes mécatroniques, vu leur complexité, nécessite d'entreprendre une approche systémique. Une approche systémique implique l'utilisation d'une méthodologie permettant, en premier lieu, de considérer le système avec toutes ses composantes (mécanique, électronique, informatique, etc.) et de fournir les moyens de concevoir et de spécifier ce système par la définition de ses composants et des liens qui existent entre eux. D'autre part, cette méthodologie doit aussi donner la possibilité de décrire ces composants avec les outils existants dédiés aux domaines technologiques. Nous nous sommes tournés vers des technologies orientées-objet, en l'occurrence l'ingénierie guidée par les modèles MDE, pour construire une méthodologie permettant d'entreprendre cette approche systémique supportant les activités d'ingénierie décrites dans le standard ISO/IEC/IEEE 15288. Dans cette thèse, nous proposons donc une méthodologie qui répond à ces besoins et que nous avons intitulé MISSyM. Dans MISSyM, les activités de conception sont réalisées sur des modèles SysML étendus par des profiles supportant le standard ISO/IEC/IEEE 15288. De plus, MISSyM intègre le support d'éléments de modélisation spécifiques aux systèmes mécatroniques qui sont le composant mécatronique ainsi que des extensions et des design pattern spécifiques. Nous avons aussi intégré dans MISSyM une extension au langage SysML supportant les Bond Graphs et permettant d'entreprendre une analyse énergétique des systèmes hétérogènes. Nous avons par la suite enrichi la méthodologie MISSyM par une méthode de vérification de la qualité de l'architecture qui repose sur un algorithme utilisant des métriques sur les modèles décrivant l'architecture d'un composant donné ou du système puis appliquant un algorithme de partitionnement de la matrice de dépendances ou DSM (existant) pour proposer une amélioration de cette architecture. Nous avons en plus fourni l'ouverture vers le langage de simulation Modelica par la génération de code. Et finalement, nous avons décrit le processus global de la méthodologie basé sur l'architecture de modèles MDA et en concordance avec le standard d'ingénierie système ISO/IEC/IEEE 15288. Nous avons fourni un exemple d'application pour permettre aux ingénieurs système de mieux utiliser le nouveau langage SysML à travers cette méthodologie.

Mes travaux de thèse s'articulaient autour de la validation de modèles et de programmes. En ce sens, les modèles sont validés par animation, de manière à s'assurer qu'ils décrivent le bon comportement du système qu'ils représentent. Il s'agit d'un processus semi-automatique, car l'utilisateur sélectionne les actions du système à exécuter et effectue la comparaison entre les descriptions informelles données dans le cahier des charges et les résultats produits par le modèle. Un modèle validé est ensuite utilisé dans l'objectif de produire des cas de tests fonctionnels destinés à être joués sur une implantation ou un système sous test. Le modèle formel est ainsi utilisé à deux niveaux : d'une part, il permet de calculer de manière automatique les suites de tests, et, d'autre part, il sert d'oracle pour établir le verdict du test.<br />Au cours de ces travaux, nous nous sommes intéressés à la validation de programmes Java par l'intermédiaire de son langage de modélisation associé, nommé JML. Suite aux expériences et aux savoirs-faire accumulés au sein de l'équipe Techniques Formelles et à Contraintes du Laboratoire d'Informatique de Franche-Comté, nous avons choisi d'appliquer une représentation logico-ensembliste des modèles JML, reposant sur des solveurs de contraintes pour gérer les valeurs des variables des modèles objets que nous traitons. A partir de cette représentation symbolique, nous avons exprimé l'animation symbolique d'un modèle objet basé sur la sémantique de Java, utilisant les descriptions formelles contenues dans les pré- et postconditions des spécifications des méthodes.<br />Nous nous sommes ensuite appuyés sur la définition symbolique des états du système objet pour extraire des cibles de tests, liées aux comportements issus des méthodes, définies par un prédicat obtenu par conjonction de la condition d'activation du comportement et de la mise aux limites des attributs des objets du système et des paramètres de la méthode sous test. L'animation symbolique du modèle entre en jeu pour la construction des cas de tests. Un algorithme de parcours de l'espace d'états effectue la recherche d'un chemin d'exécution menant à la cible. Les cas de tests sont ensuite concrétisés pour produire un pilote de test Java. Une étude de cas a été menée sur une modélisation fonctionnelle d'un porte-monnaie électronique.<br />Ces travaux ont été implantés dans un prototype, nommé JML-Testing-Tools, qui permet l'animation symbolique d'un modèle JML et la génération de cas de tests pour l'implantation Java qui lui est associée. Ce prototype est composé d'un compilateur traduisant une spécification JML et des signatures de classes Java dans un format logico-ensembliste. Le modèle décrit dans ce format est ensuite animé par un interpréteur rétablissant la sémantique opérationnelle du Java/JML.

L'objectif de cette thèse est de faciliter la conception et le déploiement d'applications distribuées sur la Grille, en utilisant une approche orientée composants. Les problématiques du calcul sur grilles abordées dans notre proposition sont : la complexité de conception, le déploiement, la flexibilité et la performance. Nous proposons et justifions un modèle de composants et son implantation. Le modèle proposé repose sur le modèle de composants Fractal et sur le modèle des objets actifs. Il bénéficie d'une part, de la structure hiérarchique et de la définition précise du modèle Fractal, et d'autre part, de l'identification des composants comme activités configurables. Nous proposons un modèle de déploiement et nous spécifions un ensemble de primitives pour les communications collectives, grâce à la définition d'interfaces collectives. Les interfaces collectives permettent de gérer la distribution des données, le parallélisme et la synchronisation des invocations.<br />Nous avons développé une implantation du modèle proposé avec l'intergiciel de grille ProActive. Le framework de composants bénéficie ainsi des fonctionnalités sous-jacentes offertes par l'intergiciel ProActive. Nous démontrons la capacité de passage à l'échelle et l'efficacité de notre framework en déployant sur plusieurs centaines de machines des applications intensives en termes de calcul et de communications. Nous mettons à profit les interfaces collectives pour développer une application SPMD à base de composants, dont nous évaluons les performances.

The capability to easily find useful services (software applications, software components, scientific computations) becomes increasingly critical in several fields. Current approaches for services retrieval are mostly limited to the matching of their inputs/outputs possibly enhanced with some ontological knowledge. Recent works have demonstrated that this approach is not sufficient to discover relevant components. In this dissertation we argue that, in many situations, the service discovery should be based on the specification of service behavior. The idea behind it, is to develop matching techniques that operate on behavior models and allow delivery of partial matches and evaluation of semantic distance between these matches and the user requirements. Consequently, even if a service satisfying exactly the user requirements does not exist, the most similar ones will be retrieved and proposed for reuse by extension or modification. To do so, we reduce the problem of behavioral matching to a graph matching problem and we adapt existing algorithms for this purpose. <br /><br />Motivated by these concerns, we developed the WS-BeM platform for ranking web services based on behavior matchmaking, which takes as input two WSCL or BPEL protocols and evaluates the semantic distance between them. The prototype is also available as a web service. Furthermore, an application is described concerning the tool for evaluating the effectiveness of the behavioral matchmaking method.