Dans notre travail nous nous sommes intéressés à la vérification<br /> automatique de propriétés comportementales d'applications réparties par des<br /> méthodes fondées sur les<br />modèles. En particulier, nous étudions le problème de<br />génération de modèles <br />à partir de programmes Java répartis et représentés par des systèmes de transitions<br />communiquants.<br /><br />Pour ce faire, nous définissons une sémantique comportementale de programmes ProActive, une<br />librairie Java pour la programmation parallèle, distribuée et<br />concurrente. À partir de cette sémantique nous construisons des modèles<br />comportementaux pour<br />des abstractions finies d'applications écrites dans ce langage. Ces<br />modèles sont basés sur la sémantique des algèbres de<br />processus et peuvent donc être construits de manière compositionnelle et<br />hiérarchique.<br />La construction de modèles finis n'est pas toujours possible. Pour<br />pouvoir traiter des problèmes prenant en compte des données, ainsi que<br />des problèmes concernant des topologies non bornées d'objets<br />répartis, nous définissons une nouvelle notion de modèleles<br />hiérarchiques, à base de systèmes de transitions paramétrés et de<br />réseau de synchronisation paramétrés. Moyennant des abstractions ces modèles permettent de<br />spécifier des applications possiblement infinies par des représentations<br />expressives, finies, et plus proche de la structure du code. <br />Par ailleurs, nous définissons un système de règles sémantiques<br />permettant de générer automatiquement ces modèles (finis ou<br />paramétrés) à partir d'une forme intermédiaire, obtenue par analyse statique,<br />des programmes analysés.<br />Les modèles ainsi générés sont exploitables directement ou après<br />instantiation par des outils de vérification.

Cette thèse est consacrée au problème de la vérification automatique des protocoles cryptographiques d'un point de vue logique et calculatoire.<br />Dans une première partie, nous abordons la sécurité des protocoles dans le cadre logique (formel). Nous montrons comment spécifier différentes propriétés de sécurité des protocoles (secret, authentification, <br />résistance aux attaques par dictionnaire) au moyen d'un langage de processus et comment les analyser de manière automatique pour un nombre borné de sessions.<br />La seconde partie traite de la justification cryptographique des modèles logiques. Nous nous intéressons ici à la notion d'équivalence statique, appliquée en particulier au chiffrement et aux données vulnérables aux attaques par dictionnaire (par ex. des mots de passe). Dans ce cadre, nous montrons que sous certaines conditions simples, toute preuve logique d'équivalence statique implique d'indistinguibilité cryptographique des données modélisées.

Les comportement épistémiques, mobiles et spatiaux sont omniprésent dans les systèmes distribués aujourd’hui. La nature intrinsèque épistémique de ces types de systèmes provient des interactions des éleménts qui en font parties. La plupart des gens sont familiarisés avec des systèmes numériques où les utilisateurs peuvent partager ses croyances, opinions et même des mensonges intentionnels (des canulars). Aussi, les modèles de ces systèmes doivent tenir compte des interactions avec d’autres de même que leur nature distribués. Ces comportements spatiaux et mobiles font part d’applications où les données se déplacent dans des espaces (peut-être imbriqués) qui sont définis par, par exemple, cercles d’amis, des groupes, ou des dossiers partagés. Nous pensons donc qu’une solide compréhension des notion d’espaces, de mobilité spatial ainsi que le flux d’information épistémique est cruciale dans la plupart des modèles de systèmes distribués de nos jours.Les systèmes de contrainte (sc) fournissent les domaines et les opérations de base pour les fondements sémantiques de la famille de modèles déclaratifs formels de la théorie de la concurrence connu sous le nom de programmation concurrent par contraintes (pcc). Les systèmes des contraintes spatiales (scs) représentent des structures algébriques qui étendent sc pour raisonner sur les comportement spatiaux et épistémiques de base tel que croyance et l’extrusion. Les assertions spatiales et épistémiques peuvent être vues comme des modalités spécifiques. D’autres modalités peuvent être utilisées pour les assertions concernant le temps, les connaissances et même pour l’analyse des groupes entre autres concepts utilisés dans la spécification et la vérification des systèmes concurrents.Dans cette thèse nous étudions l’expressivité des systèmes de contraintes spatiales dans la perspective générale du comportement modal et épistémique. Nous montrerons que les systèmes de contraintes spatiales sont assez robustes pour capturer des modalités inverses et pour obtenir de nouveaux résultats pour les logiques modales. Également, nous montrerons que nous pouvons utiliser les scs pour exprimer un comportement épistémique fondamental comme connaissance. Finalement, nous donnerons une caractérisation algébrique de la notion de l’information distribuée au moyen de constructions sur scs. / Epistemic, mobile and spatial behaviour are common place in today’s distributed systems. The intrinsic epistemic nature of these systems arises from the interactions of the elements taking part of them. Most people are familiar with digital systems where users share their beliefs, opinions and even intentional lies (hoaxes). Models of those systems must take into account the interactions with others as well as the distributed quality these systems present. Spatial and mobile behaviour are exhibited by applications and data moving across (possibly nested) spaces defined by, for example, friend circles, groups, and shared folders. We therefore believe that a solid understanding of the notion of space and spatial mobility as well as the flow of epistemic information is relevant in many models of today’s distributed systems.Constraint systems (cs’s) provide the basic domains and opera- tions for the semantic foundations of the family of formal declarative models from concurrency theory known as concurrent constraint programming (ccp). Spatial constraint systems (scs’s) are algebraic structures that extend cs’s for reasoning about basic spatial and epistemic behaviour such as belief and extrusion. Both spatial and epistemic assertions can be viewed as specific modalities. Other modalities can be used for assertions about time, knowledge and even the analysis of groups among other concepts used in the specification and verification of concurrent systems.In this thesis we study the expressiveness of spatial constraint systems in the broader perspective of modal and epistemic behaviour. We shall show that spatial constraint systems are sufficiently robust to capture inverse modalities and to derive new results for modal logics. We shall show that we can use scs’s to express a fundamental epistemic behaviour such as knowledge. Finally we shall give an algebraic characterization of the notion of distributed information by means of constructors over scs’s.

Qu'il s'agisse de téléphones portables ou de serveurs web, d'applets ou de paquets réseau, les systèmes matériels et logiciels sont contraints par des limitations sur les ressources telles que la mémoire, l'utilisation du disque ou les connexions au réseau. En particulier, il est nécessaire de contrôler l'allocation et la désallocation des ressources ainsi que le respect de protocoles, afin de prévenir les dépassements de capacité ou d'autres formes d'attaque ou d'accidents. Ce aspect, pourtant central dans la conception d'applications mobiles et communicantes, est ignoré par la majorité des algèbres de processus. Afin de contribuer à résoudre ce problème, nous avons étudié la notion de ressources. Nous avons formalisé cette notion dans le contexte de calculs conçus autour de la mobilité de sites, tels que les Mobile Ambients, ou de la mobilité de noms, comme le pi-calcul. Nous avons ainsi mis en évidence les mécanismes d'allocation et de désallocation de ressources et dégagé des méthodes pour prendre en compte les ressources et de les réutiliser intelligemment. De plus, les systèmes de types que nous avons conçus permettent de garantir statiquement qu'un système, au cours de son exécution, ne nécessitera pas plus de ressources qu'il n'est autorisé à en utiliser.

Nous présentons un système de retour arrière distribué basé sur le Calcul des Systèmes Communicants de Robin Milner. L'algèbre de pro- cessus réversible ainsi définie (RCCS) nous permet de poser les fondements théoriques du retour arrière dans un calcul concurrent. En particulier, étant donné un processus et un passé, nous montrons que RCCS permet de re- venir en arrière dans tout passé causalement équivalent. Nous exprimons aussi l'équivalence comportementale associée aux processus réversibles en utilisant une notion de bisimulation mettant en relation les traces causales des processus. Il en résulte une méthode de programmation déclarative de systèmes transactionnels qui peuvent être efficacement vérifiés à l'aide d'un algorithme basé sur des structures d'événements. Par l'intermédiaire d'une construction catégorique, nous montrons que cette méthode peut être géné- ralisée à une large classe de calculs concurrents.

Dans cette thèse, trois calculs de processus sont étudiés et appliqués à l'analyse de processus biologiques : une variante du π -calcul introduite ici, le Iπ-calcul; le κ-calcul de Danos et Laneve et sa variante à grain plus fin, le mκ-calcul; et les systèmes réactifs bigraphiques de Milner. Le manuscrit comporte trois parties. <br />Dans la première partie, nous modélisons la transduction du signal, et plus spécifiquement le processus d'activation de la protéine "ras". On introduit une nouvelle extension du π-calcul, le Iπ-calcul, pour modéliser ce processus biologique en présence d'aberrance. Le calcul est obtenu en ajoutant deux actions aberrantes au Iπ-calcul. Le Iπ-calcul, quoique déjà assez expressif pour exprimer l'aberrance, peut être encore précisé par l'introduction d'informations supplémentaires dans la syntaxe, soit sous forme de "tags" soit sous forme de types. Les tags sont plus intuitifs, mais ils introduisent de la redondance, qui est éliminée dans la présentation de cette information sous forme de types. Nous montrons l'équivalence entre les deux espèces de décoration. Le système de types / tags présenté ici est très rudimentaire, mais notre espoir est de l'enrichir pour intégrer des paramètres quantitatifs tels que la température, la concentration, etc... dans la modélisation des processus biologiques.<br />Dans la seconde partie, nous abordons d'un point de vue formel la question de l'auto-assemblage dans le κ-calcul, un langage de description d'interactions protéine-protéine. Nous définissons un sous-ensemble de règles de calcul réversibles nous permettant d'assurer un codage sans blocage du calcul "à gros grain" (le κ-calcul) dans un calcul "à grain fin" (le mκ-calcul). Nous prouvons la correction de cette simulation de manière interne (à l'aide des règles réversibles), améliorant ainsi les résultats de Danos et Laneve.<br />Enfin, dans une partie plus prospective, nous suggérons comment l'on peut utiliser les bigraphes pour modéliser et analyser les processus biologiques. Nous montrons d'abord commment coder l'exemple "ras" dans ce formalisme. Puis nous indiquons sur un exemple comment l'on peut traduire le κ--calcul dans les bigraphes.

Durant leur exécution, les systèmes concurrents manipulent diverses ressources dynamiques en nombre : fichiers, liens de communication, mémoire, etc. Les propriétés comportementales de ces systèmes sont alors étroitement liées aux manipulations de ces ressources qu'ils allouent, utilisent, puis détruisent. Nous proposons dans cette thèse une analyse quantitative, effectuée de manière statique, de ce type de ressources pour les systèmes concurrents et dynamiques. Les systèmes que l'on considère peuvent être des programmes concurrents et parallèles (le langage Piccolo développé dans le cadre de ce travail en est un exemple), ou encore la modélisation de systèmes plus généraux. Pour atteindre cette généricité, notre travail repose fortement sur les algèbres de processus, et plus particulièrement sur le pi-calcul pour lequel nous proposons une variante sémantique ainsi que plusieurs abstractions adaptées à l'observation des ressources en particulier. Le socle théorique de notre analyse est présenté sous la forme d'un nouveau type d'automates nominaux : les nu-automates. Ils permettent de raisonner spécifiquement sur les ressources dynamiques, tant pour caractériser les notions quantitatives de consommation en ressources que pour de futures analyses qualitatives. À partir de ce formalisme nous réalisons ensuite un ensemble d'algorithmes ayant pour but de mettre en oeuvre les résultats introduits sur les nu-automates. Enfin, nous proposons plusieurs expérimentations, sur la base d'exemples classiques du pi-calcul, de notre prototype d'analyse de ressources. / Concurrent activities involve undoubtedly many dynamic resources manupulations: files, communication links, memory, etc. Then, the behavioral properties of such systems are closely linked to their usage of those resources that they allocate, use, and finally destroy. In this work, we develop a quantitative static analysis of concurrent and parallel systems for this kind of resources. Systems that we consider can be concurrent and parallel programs (written for example in the Piccolo programming language which was developped during this thesis), or models descriptions of more general systems. To be generic, our work lies on process algebra, specifically pi-calculs for which we propose a variant semantics in addition to several resources abstractions strategies. The underlying theory is developped as a nominal automata framework (namely the nu-automata). They allow one to reason about dynamic resources usage to charaterize both quantitative and qualitative properties. From this formalism we establish an algorithmic framework that enforce the qualitative results defined on nu-automata. Finally, our resources abstractions and resources analysis are tested experimentally on classical pi-calculus examples using our prototype analysis tool.

La construction de programmes nécessite l'utilisation d'outils adaptés. Un outil particulier est le langage de programmation. Les langages logico-fonctionnels sont des langages de programmation dits déclaratifs qui se basent sur les notions mathématiques de fonction et de prédicat. Ce fondement théorique solide facilite à la fois la description d'un système à un niveau proche de la spécification ainsi que la validation de programmes. Néanmoins, les concepts sous-jacents aux langages logico-fonctionnels sont insuffisants pour la description aisée de systèmes complexes qui nécessitent l'interactivité, la concurrence et la distribution. Pour la modélisation de ces systèmes, la notion de processus a été introduite. Dans le contexte des algèbres de processus, un processus est caractérisé par les actions qu'il est capable d'exécuter. Cependant, les langages fondés uniquement sur les algèbres de processus doivent être étendus afin d'éviter le codage de fonctions et de prédicats en termes de processus. Dans cette thèse nous proposons un modèle de calcul qui intègre la programmation concurrente et déclarative. Nous suggérons de modéliser un système par un ensemble de composants. Chacun de ces composants comporte un programme déclaratif, appelé store, et un ensemble de processus interagissant par l'exécution d'actions. De plus, un composant peut contenir de nouvelles actions définissables par le programmeur. L'interaction entre composants est fondée sur le même principe, c.-à.-d. un processus peut exécuter des actions sur les stores des autres composants. Les différents composants d'un système peuvent utiliser des langages déclaratifs différents pour la description de leurs stores respectifs, ce qui nécessite la traduction des valeurs communiquées. Nous donnons une sémantique compositionnelle ainsi qu'une analyse de la confidentialité pour les processus d'un composant, et présentons les principes d'un prototype implanté

Dans cette thèse, nous proposons un langage formel, le gk-calcul, issu de la famille des algèbres de processus. Ce langage se distingue notamment des langages concurrents habituels par la rupture de la dissymétrie inhérente à la notion d'émetteur et de récepteur traditionnellement considérée. Cette rupture permet alors de voir les interactions entre les éléments du langage comme des phénomènes de collisions, approche bien adaptée aux questions d'auto-organisation qui font l'objet de la première partie de cette thèse.<br /><br />La question qui se pose est celle de la construction concurrente et décentralisée de formes géométriques abstraites (arbres et graphes) ainsi que de phénomènes plus génériques décrits sous forme de transfert d'information dans des systèmes à base de réécriture de graphes, éventuellement hiérarchisés dans l'optique d'une application à la biologie moléculaire. Cette première partie s'accompagne notamment d'une implémentation en Ocaml simulant un algorithme d'auto-assemblage de graphes.<br /><br />Dans un second temps, nous développons un sous-ensemble du langage présenté, en enrichissant une version restreinte aux interactions binaires avec une notion de membrane et d'interactions entre membranes. Ce nouveau langage se montre à même de décrire une biologie moléculaire simplifiée, qualitative, basée sur les interactions entre protéines et membranes. Cette partie de la thèse s'attache alors à montrer la valeur descriptive de ce langage sur quelques exemples et à explorer des définitions pertinentes d'équivalence entre solutions biologiques.

Nous nous intéressons à l'analyse des exigences de performabilité des systèmes communicants mobiles par model checking. Nous modélisons ces systèmes à l'aide d'un formalisme de haut niveau issu du π-calcul, permettant de considérer des comportements stochastiques, temporels, déterministes, ou indéterministes. Cependant, dans le π-calcul, la primitive de communication de base des systèmes est la communication en point-à-point synchrone. Or, les systèmes mobiles, qui utilisent des réseaux sans fil, communiquent essentiellement par diffusion locale. C'est pourquoi, dans un premier temps, nous définissons la communication par diffusion dans le π-calcul, afin de mieux modéliser les systèmes que nous étudions. Nous proposons d'utiliser des versions probabilistes et stochastiques de l'algèbre que nous avons défini, pour permettre des études de performance. Nous en définissons une version temporelle permettant de considérer le temps dans les modèles. Mais l'absence d'outils d'analyse des propriétés sur des modèles spécifiés en une algèbre issue du π-calcul est un obstacle majeur à notre travail. La définition de règles de traduction en langage PRISM, nous permet de traduire nos modèles, en modèles de bas niveau supports du model checking, à savoir des chaînes de Markov à temps discret, à temps continu, des automates temporisés, ou des automates temporisés probabilistes. Nous avons choisi l'outil PRISM car, à notre connaissance, dans sa dernière version, il est le seul outil à supporter les formalismes de bas niveau que nous venons de citer, et ainsi il permet de réaliser des études de performabilité complètes. Cette façon de procéder nous permet de pallier à l'absence d'outils d'analyse pour nos modèles. Par la suite, nous appliquons ces concepts théoriques aux réseaux de capteurs sans fil mobiles.