Les comportements des processus concurrents peuvent être exprimés en utilisant des calculs de processus, des langages formels simples qui permettent de démontrer des résultats mathématiques précis sur les interactions entre processus. Un exemple très simple est CCS, un autre exemple est le pi-calcul, plus expressif grâce à un mécanisme de communication de canaux. Dans ce dernier, on peut instaurer un système de types (pour raffiner l'analyse aux environnements plus contraints) et encoder le lambda-calcul (qui représente les calculs séquentiels).Certains de ces calculs, comme CCS ou des variantes du pi-calcul comme les calculs de fusions, ont une certaine propriété de symétrie. On utilise dans un premier temps cette symétrie comme un outil, pour prouver que deux encodages du lambda-calcul dans le pi-calcul sont en fait équivalents.Cette preuve nécessitant un système de types et une forme de symétrie, on se pose la question de l'existence d'un système de types pour les autres calculs symétriques, notamment les calculs de fusion, à laquelle on répond par la négative avec un théorème d'impossibilité.En analysant ce théorème, on découvre un contrainte fondamentale de ces calculs qui empêche l'utilisation des types, à savoir la présence d'une notion de relation d'équivalence entre les canaux de communication. Le relâchement de cette contrainte pour obtenir une relation de pré-ordre engendre un calcul intéressant qui recouvre des notions importantes du pi-calcul, absentes dans les calculs de fusion : les types et les noms privés. La première partie de la thèse se concentre sur l'étude de ce calcul.La deuxième partie de la thèse se concentre sur la bisimulation, une méthode pour établir l'équivalence de deux agents dans des langages d'ordre supérieur, par exemple le pi-calcul ou le lambda-calcul. Une amélioration de cette méthode est la théorie des techniques modulo, très puissante, mais qui malheureusement s'applique uniquement aux systèmes de premier ordre, comme les automates ou CCS.Cette thèse s'applique alors à décrire les langages d'ordre supérieur en tant que systèmes du premier ordre. On récupère ainsi la théorie générale des techniques modulo pour ces langages, en prouvant correctes la correspondance induite et les techniques spécifiques à chaque langage. On détaille les tenants et aboutissants de cette approche, pour fournir les outils nécessaires à son utilisation pour d'autres langages d'ordre supérieur. / The behaviours of concurrent processes can be expressed using process calculi, which are simple formal languages that let us establish precise mathematical results on the behaviours and interactions between processes. A very simple example is CCS, another one is the pi-calculus, which is more expressive thanks to a name-passing mechanism. The pi-calculus supports the addition of type systems (to refine the analysis to more subtle environments) and the encoding of the lambda-calculus (which represents sequential computations).Some of these calculi, like CCS or variants of the pi-calculus such as fusion calculi, enjoy a property of symmetry. First, we use this symmetry as a tool to prove that two encodings of the lambda-calculus in the pi-calculus are in fact equivalent.This proof using a type system and a form of symmetry, we wonder if other existing symmetric calculi can support the addition of type systems. We answer negatively to this question with an impossibility theorem.Investigating this theorem leads us to a fundamental constraint of these calculi that forbids types: they induce an equivalence relation on names. Relaxing this constraint to make it a preorder relation yields another calculus that recovers important notions of the pi-calculus, that fusion calculi do not satisfy: the notions of types and of privacy of names. The first part of this thesis focuses on the study of this calculus, a pi-calculus with preorders on names.The second part of this thesis focuses on bisimulation, a proof method for equivalence of agents in higher-order languages, like the pi- or the lambda-calculi. An enhancement of this method is the powerful theory of bisimulations up to, which unfortunately only applies for first-order systems, like automata or CCS.We then proceed to describe higher-order languages as first-order systems. This way, we inherit the general theory of up-to techniques for these languages, by proving correct the translations and up-to techniques that are specific to each language. We give details on the approach, to provide the necessary tools for future applications of this method to other higher-order languages.

Le comportement d'une cellule dépend de sa capacité à recevoir, propager et intégrer des signaux, constituant ainsi des voies de signalisations. Les protéines s'associent entre elles sur des sites de liaisons, puis modifient la structure spatiale des protéines voisines, ce qui a pour effet de cacher ou de découvrir leurs autres sites de liaisons, et donc d'empêcher ou de faciliter d'autres interactions. En raison du grand nombre de différents complexes bio-moléculaires, nous ne pouvons pas écrire ou générer les systèmes différentiels sous-jacents. Les langages de réécritures de graphes à sites offrent un bon moyen de décrire ces systèmes complexes. Néanmoins la complexité combinatoire resurgit lorsque l'on cherche à calculer de manière effective ce comportement. Ceci justifie l'utilisation d'abstractions. Nous proposons deux méthodes pour réduire la taille des modèles de voies de signalisation, décrits en Kappa. Ces méthodes utilisent respectivement la présence de symétries parmi certains sites et le fait que certaines corrélations entre l'état de différentes parties des complexes biomoléculaires n'ont pas d'impact sur la dynamique du système global. Des sites qui ont la même capacité d'interaction sont liés par une relation de symétrie. Nous montrons que cette relation induit une bisimulation qui peut être utilisée pour réduire la taille du modèle initial. L'analyse du flot d'information détecte les parties du système qui influencent le comportement de chaque site. Ceci nous autorise à couper les espèces moléculaires en petits morceaux pour écrire un nouveau système. Enfin, nous montrons comment raffiner cette analyse pour tenir compte d'information contextuelle. Les deux méthodes peuvent être combinées. La solution analytique du modèle réduit est la projection exacte de la solution originelle. Le calcul du modèle réduit se fait au niveau des règles, en évitant l'exécution du modèle initial. / The behaviour of a cell is driven by its capability to receive, propagate and communicate signals. Proteins can bind together on some binding sites. Post-translational modifications can reveal or hide some sites, so new interactions can be allowed or existing ones can be inhibited. Due to the huge number of different bio-molecular complexes, we can no longer derive or integrate ODE models. A compact way to describe these systems is supplied by rule-based languages. However combinatorial complexity raises again when one attempt to describe formally the behaviour of the models. This motivates the use of abstractions. We propose two methods to reduce the size of the models, that exploit respectively the presence of symmetries between sites and the lack of correlation between different parts of the system. The symmetries relates pairs of sites having the same capability of interactions. We show that this relation induces a bisimulation which can be used to reduce the size of the original model. The information flow analysis detects, for each site, which parts of the system influence its behaviour. This allows us to cut the molecular species in smaller pieces and to write a new system. Moreover we show how this analysis can be tuned with respect to a context. Both approaches can be combined. The analytical solution of the reduced model is the exact projection of the original one. The computation of the reduced model is performed at the level of rules, without the need of executing the original model.

Dans cette thèse nous proposons un cadre formel complet pour l'analyse des systèmes temporisés, avec l'accent mis sur la valeur pratique de l'approche. Nous décrivons des systèmes comme des automates temporisés et nous exprimons les propriétés en logiques temps-réel. Nous considérons deux types d'analyse. Vérification : étant donnés un système et une propriété, vérifier que le système satisfait la propriété. Synthèse de contrôleurs : étant donnés un système et une propriété, restreindre le système pour qu'il satisfasse la propriété. Pour rendre l'approche possible malgré la difficulté théorique des problèmes, nous proposons : Des abstractions pour réduire l'espace d'états concret en un espace abstrait beaucoup plus petit qui, pourtant, préserve toutes les propriétés qui nous intéressent. Des techniques efficaces pour calculer et explorer l'espace d'états abstrait. Nous définissons des bisimulations et simulations faisant abstraction du temps et nous étudions les propriétés qu'elles préservent. Pour les bisimulations, l'analyse consiste à générer d'abord l'espace abstrait, et ensuite l'utiliser pour vérifier des propriétés sur l'espace concret. Pour les simulations, la génération et la vérification se font en même temps (à-la-volée). Un algorithme à-la-volée est aussi développé pour la synthèse de contrôleurs. Pour aider l'utilisateur à sa compréhension du système, nous produisons des séquences diagnostiques concrètes. Nous avons implanté nos méthodes dans Kronos, l'outil d'analyse temps-réel de Verimag, et nous avons traité un nombre d'études de cas réalistes parmi lesquelles le protocole FRP-DT de réservation rapide de débit pour les réseaux ATM (dans le cadre d'une coopération scientifique avec le CNET), le protocole de détection de collisions dans un réseaux à accès multiple de Band&Olufsen, l'ordonnancement de tâches temps-réel périodiques, la cohérence et l'ordonnancement des documents multimédia, ainsi qu'un nombre d'études de cas benchmarks, telles que le protocole d'exclusion mutuelle de Fischer, les protocoles de communication CSMA/CD et FDDI.