La perméabilité membranaire joue un rôle important dans la résistance aux antibiotiques chez lesbactéries à Gram négatif.L’objectif de notre travail était de caractériser la fonction tenue par les deux régulateurs globaux dela perméabilité membranaire chez Enterobacer aerogenes: mar et ram. L’objectif initial futd’identifier le répresseur spécifique de RamA qui manquait en tant qu’élément de la cascade derégulation actuellement définie. La sélection de 60 souches nous a permis de confirmer le rôlecentral joué par RamA dans la régulation, ainsi qu’identifier des mutations pouvant être critiques, auniveau de RamR. Ainsi, l’absence variations observées dans le régulon marRAB et l’expressionmodérée des transcrits montrée par qRT-PCR laisse penser, que RamA a un rôle clef dans larégulation de l’expression des porines et des pompes d’efflux chez E. aerogenes.L’autre partie de notre travail reposait sur l’étude de la translocation des antibiotiques au traversdes porines. L’étude des interactions porine-carbapénèmes s’est faite sur la porine sauvage OmpFd'Escherichia coli et deux mutations. Les résultats indiquent également l'importance de l'aspartateen position 113 dans la sélectivité de translocation des carbapénèmes au sein de la porine OmpF.Ce travail montre ainsi que la translocation des pénicillines est aussi sous la dépendance desinteractions qui se créent entre le substrat et le résidu en position 113 de OmpF et limitent alorsleur passage au niveau du canal porine. Nous avons recherché la contribution attribuée à la porineOmp36 d'E. aerogenes dans la translocation de certaines béta-lactamines. Les mesures ont permisde conclure que les deux beta-lactamin / Genetic permeability plays an important role in antibiotic resistance of Gram-negative bacteria.Our work was to characterize and better understand of the genetic regulation of membranepermeability in E. aerogenes. We focused on two global regulators, mar and ram, in about 60clinical isolates. Alterations in the upstream region of ramA and in ramR but no mutations in marAnor marR were observed. Overexpression of ramA or ramR led to an altered antibiotic susceptibilityassociated to decrease of porins expression and over-expression of efflux-pumps. qRT-PCR pointedout the estimated importance of the ram-regulon in the regulation cascade.Another part of this work was to characterize the translocation of compounds through porins andthe role of porins in drug uptake in general. Measurement of the rate of antibiotic action of threecarbapenems in an E. coli strain solely expressing OmpF as porin clearly indicated the importanceof the aspartate at position 113 in antibiotic translocation. A multi-disciplinary three way approachof computer modeling, black-lipid-bilayer assays and measurement of antibiotic action, suggestedthat interactions with residue D113 of E. coli porin OmpF are rate-limiting for transport throughthe porin channel. Combination of biological and biophysical measurements with E. aerogenesporin Omp36 denoted that interactions between the porin channel and the antibiotic facilitate andaccelerate transport.

Dans ce mémoire, nous présentons l’utilisation de techniques de model-checking pour l’inférence de paramètres de réseaux de régulation génétique (GRN) et l’analyse formelle d’une voie de signalisation. Le coeur du mémoire est décrit dans la première partie, dans laquelle nous proposons une approche pour inférer les paramètres biologiques régissant les dynamiques de modèles discrets de GRN. Les GRN sont encodés sous la forme d’un méta-modèle, appelé GRN paramétré, de telle façon qu’une instance de paramètres définit un modèle discret du GRN initial. Sous réserve que les propriétés biologiques d’intérêt s’expriment sous la forme de formules LTL, les techniques de model-checking LTL sont combinées à celles d’exécution symbolique et de résolution de contraintes afin de sélectionner les modèles satisfaisant ces propriétés. L’enjeu est de contourner l’explosion combinatoire en terme de taille et de nombre de modèles discrets. Nous avons implémenté notre méthode en Java, dans un outil appelé SPuTNIk. La seconde partie décrit une collaboration avec des neuropédiatres, qui ont pour objectif de comprendre l’apparition du phénotype protecteur ou toxique des microglies (un type de macrophage du cerveau) chez les prématurés. Cette partie exploite un autre versant du model-checking, celui du modelchecking statistique, afin d’étudier un type de réseau biologique particulier : la voie de signalisation Wnt/β-caténine, qui permet la transmission d’un signal de l’extérieur à l’intérieur des cellules via une cascade de réactions biochimiques. Nous présentons ici l’apport du model-checker stochastique COSMOS, utilisant la logique stochastique à automate hybride (HASL), un formalisme très expressif nous permettant une analyse formelle sophistiquée des dynamiques de la voie Wnt/β-caténine, modélisée sous la forme d’un processus stochastique à événements discrets. / In this thesis, we present the use of model checking techniques for inference of parameters of Gene Regulatory Networks (GRNs) and formal analysis of a signalling pathway. In the first and main part, we provide an approach to infer biological parameters governing the dynamics of discrete models of GRNs. GRNs are encoded in the form of a meta-model, called Parametric GRN, such that a parameter instance defines a discrete model of the original GRN. Provided that targeted biological properties are expressed in the form of LTL formulas, LTL model-checking techniques are combined with symbolic execution and constraint solving techniques to select discrete models satisfying these properties. The challenge is to prevent combinatorial explosion in terms of size and number of discrete models. Our method is implemented in Java, in a tool called SPuTNIk. The second part describes a work performed in collaboration with child neurologists, who aim to understand the occurrence of toxic or protective phenotype of microglia (a type of macrophage in the brain) in the case of preemies. We use an other type of model-checking, the statistical model-checking, to study a particular type of biological network: the Wnt/β- catenin pathway that transmits an external signal into the cells via a cascade of biochemical reactions. Here we present the benefit of the stochastic model checker COSMOS, using the Hybrid Automata Stochastic Logic (HASL), that is an very expressive formalism allowing a sophisticated formal analysis of the dynamics of the Wnt/β-catenin pathway, modelled as a discrete event stochastic process.

Cette thèse concerne l'ingénierie des systèmes complexes à partir d'une dynamique souhaitée. En particulier, nous nous intéressons aux populations d'oscillateurs et aux réseaux de régulation génétique. Dans une première partie, nous nous fondons sur une hypothèse, introduite en neurosciences, qui souligne le rôle de la synchronisation neuronale dans le traitement de l'information cognitive. Nous proposons de l'utiliser sur un plan plus large pour étudier le traitement de l'information par des populations d'oscillateurs. Nous discutons des isochrons de quelques oscillateurs classés selon leurs symétries dans l'espace des états. Cela nous permet d'avoir un critère qualitatif pour choisir un oscillateur. Par la suite, nous définissons des procédures d'impression, de lecture et de réorganisation de l'information sur une population d'oscillateurs. En perspective, nous proposons un système à couches d'oscillateurs de Wilson-Cowan. Ce système juxtapose convenablement synchronisation et désynchronisation à travers l'utilisation de deux formes de couplage: un couplage continu et un couplage par pulsation. Nous finissons en proposant une application de ce système: la détection de contours dans une image. En deuxième partie, nous proposons d'utiliser une approche par contraintes pour identifier des réseaux de régulation génétique à partir de connaissances partielles sur leur dynamique et leur structure. Le formalisme que nous utilisons est connu sous le nom de réseaux d'automates booléens à seuil ou réseaux Hopfield-semblables. Nous appliquons cette méthode, afin de déterminer le réseau de régulation de la morphogenèse florale d'Arabidopsis thaliana. Nous montrons l'absence d'unicité des solutions dans l'ensemble des modèles valides (ici, 532 modèles). Nous montrons le potentiel de cette approche dans la détermination et la classification de modèles de réseaux de régulation génétique. L'ensemble de ces travaux mène à un certain nombre d'applications, en particulier dans le développement de nouvelles méthodes de stockage de l'information et dans le design de systèmes de calcul non conventionnel.