L'étude des grands modèles de réseaux biologiques par l'utilisation d'outils d'analyse et de simulation conduit à un grand nombre de prédictions. Cela soulève la question de savoir comment identifier les prédictions intéressantes de nouveaux phénomènes, qui peuvent être confrontés à des données expérimentales. Les techniques de vérification formelle basées sur le model checking constituent une technologie puissante pour faire face à cette augmentation d'échelle et de complexité pour l'analyse de ces réseaux. L'application de ces techniques est par contre difficile, pour plusieurs raisons. Premièrement, le domaine de la biologie des systèmes a mis en évidence quelques propriétés dynamiques du réseau, comme la multi-stabilité et les oscillations, qui ne sont pas facilement exprimables avec les logiques temporelles classiques. Deuxièmement, la difficulté de poser des questions pertinentes et intéressantes en logique temporelle est difficile pour les utilisateurs non-experts. Enfin, la plupart des modèles existants et des outils de simulation ne sont pas capables d'appliquer des techniques de model checking d'une manière transparente. La mise en œuvre des approches développées dans ce travail contribue à enlever des obstacles pour l'utilisation de la technologie de vérification formelle en biologie. Leur application a été validée sur l'analyse et la simulation de deux modèles biologiques complexes.

Les Réseaux de Régulation Biologique (RRB) sont communément utilisés en biologie systémique pour modéliser, comprendre et contrôler les dynamiques de production des protéines au sein des cellules. Bien qu'offrant une représentation très abstraite des systèmes biologiques, l'analyse formelle de tels modèles se heurte rapidement à l'explosion combinatoire des comportements engendrés. Cette thèse traite de la modélisation, de la simulation et de la vérification formelle des grands RRB à travers l'introduction d'un nouveau formalisme : les Frappes de Processus. La simplicité de ce formalisme permet notamment l'élaboration d'analyses statiques efficaces des systèmes complexes en général. Cette thèse aborde en premier lieu le raffinement du temps dans les modèles stochastiques via l'introduction d'un facteur d'absorption de stochasticité. Ceci apporte un compromis et une flexibilité entre des spécifications temporelles et stochastiques dans les modélisations hybrides. Une simulation générique (non-markovienne) des calculs de processus est alors proposée et appliquée aux Frappes de Processus. En outre de l'analyse statique des points fixes des Frappes de Processus, cette thèse développe une interprétation abstraite de ces Frappes de Processus permettant des approximations supérieures et inférieures très efficaces de propriétés d'atteignabilité discrète. Cette analyse permet également de faire émerger des composants requis pour la satisfaction de ces propriétés, guidant ainsi le contrôle du système. D'une complexité théorique limitée, cette approche promet de supporter l'analyse de très grands RRB et constitue une ainsi contribution qui ouvre sur de multiples perspectives.

L'étude des grands modèles de réseaux biologiques par l'utilisation d'outils d'analyse et de simulation conduit à un grand nombre de prédictions. Cela soulève la question de savoir comment identifier les prédictions intéressantes de nouveaux phénomènes, qui peuvent être confrontés à des données expérimentales. Les techniques de vérification formelle basées sur le model checking constituent une technologie puissante pour faire face à cette augmentation d'échelle et de complexité pour l'analyse de ces réseaux. L'application de ces techniques est par contre difficile, pour plusieurs raisons. Premièrement, le domaine de la biologie des systèmes a mis en évidence quelques propriétés dynamiques du réseau, comme la multi-stabilité et les oscillations, qui ne sont pas facilement exprimables avec les logiques temporelles classiques. Deuxièmement, la difficulté de poser des questions pertinentes et intéressantes en logique temporelle est difficile pour les utilisateurs non-experts. Enfin, la plupart des modèles existants et des outils de simulation ne sont pas capables d'appliquer des techniques de model checking d'une manière transparente. La mise en œuvre des approches développées dans ce travail contribue à enlever des obstacles pour l'utilisation de la technologie de vérification formelle en biologie. Leur application a été validée sur l'analyse et la simulation de deux modèles biologiques complexes. / The study of large models of biological networks by means of analysis and simulation tools leads to large amounts of predictions. This raises the question of how to identify interesting predictions of novel phenomena that can be confronted with experimental data. Formal verification techniques based on model-checking have recently been used to the analysis of these networks, providing a powerful technology to keep up with this increase in scale and complexity. The application of these techniques is hampered, however, by several key issues. First, the systems biology domain brought to the fore a few properties of the network dynamics like multistability and oscillations, that are not easily expressed using classical temporal logics. Second, the problem of posing relevant and interesting questions in temporal logic, is difficult for non-expert users. Finally, most of the existing modeling and simulation tools are not capable of applying model-checking techniques in a transparent way. The approaches developed in this work lower the obstacles to the use of formal verification in systems biology. They have been validated on the analysis and simulation of two real and complex biological models. / O estudo de redes biológicas tem originado o desenvolvimento de modelos cada vez mais complexos e detalhados. O estudo de redes biológicas complexas utilizando ferramentas de análise e simulação origina grandes quantidades de previsões. Isto levanta a questão de como identificar previsões interessantes de novos fenómenos que possam ser comparados com dados experimentais. As técnicas de verificação formal baseadas em model-checking têm sido usadas na análise destas redes, fornecendo uma tecnologia poderosa para acompanhar o aumento de escala e complexidade do problema. A aplicação destas técnicas tem sido dificultada por um conjunto importante de factores. Em primeiro lugar, em biologia de sistemas têm sido tratadas diversas questões acerca da dinâmica da rede, como a multi-estabilidade e oscilações, que não são facilmente expressas usando lógicas temporais clássicas. Em segundo lugar, o problema de como elaborar perguntas relevantes em lógica temporal, é difícil para o utilizador comum. Por último, a maioria das ferramentas de modelação e simulação não estão preparadas para a aplicação de técnicas de model-checking de forma transparente. Os métodos desenvolvidos nesta tese aliviam os obstáculos no uso da verificação formal em biologia de sistemas. Estes métodos foram validados através da análise e simulação de dois modelos biológicos complexos.

La modélisation de systèmes biologiques est devenue indispensable pour comprendre les phénomènes complexes et émergents issus d'influences partiellement connues, et pour envisager de contrôler un système altéré dans le but de restaurer un comportement physiologique. Tout modèle, quel que soit son paradigme sous-jacent, fait intervenir des paramètres gouvernant sa dynamique mais les mesures expérimentales ne permettent généralement pas de les identifier et cela reste l'un des problèmes majeurs de la modélisation. Cette thèse propose une méthode automatique d'identification des paramètres dynamiques de systèmes biologiques dans un cadre de modélisation hybride. Le cadre hybride choisi découpe l'espace des phases selon l'activité des entités biologiques, et associe à chacun de ces sous-espaces une vitesse d'évolution de chacun des composants. Nous proposons une logique de Hoare en temps continu ainsi qu'un calcul de plus faible précondition qui, à partir d'observations expérimentales qualitatives et chronométriques, construit les contraintes minimales sur les paramètres du modèle pour qu’il soit compatible avec les observations. Ce calcul mène à un problème de satisfaction de contraintes sur les réels et nous montrons que celui-ci peut être résolu par le solveur AbSolute.Le prototype Holmes BioNet développé au cours de cette thèse peut non seulement automatiser le processus d'identification des valeurs des paramètres à partir des observations expérimentales, mais aussi simuler l'évolution du modèle obtenu afin de le comparer avec les traces expérimentales. Nous utilisons ce prototype pour modéliser le couplage des cycles cellulaire et circadien. / Modelling biological systems has become instrumental to understand complex and emerging phenomena resulting from partially known influences, and to consider controlling an altered system in order to restore a physiological behaviour. Any model, independent of the underlying paradigm, involves parameters governing its dynamics. However, experimental measurements generally do not allow their identification and this remains one of the major problems of modelling. This PhD proposes an automatic method for identifying the dynamic parameters of biological systems in a hybrid modelling framework. The chosen hybrid framework splits the phase space according to the activity of the biological entities, and associates to each of these subspaces a celerity for each of the components. We introduce a continuous time Hoare logic as well as its weakest precondition calculus which, from qualitative and chronometrical experimental observations, constructs the minimum constraints on the model parameters making it compatible with the observations. This calculus leads to a Constraint Satisfaction Problem on real numbers and we show that it can be solved by the AbSolute solver.The Holmes BioNet prototype developed during this PhD can not only automate the parameter identification process from experimental data, but also simulate the evolution of the obtained model in order to compare it with experimental traces. We use this prototype to model the coupling of the cellular and circadian cycles.

L’agroécologie offre de nouvelles perspectives à l’agriculture et ainsi une voie vers une gestion alternative des adventices à travers différents mécanismes écosystémiques de régulation. La prédation des graines est l’un d’entre eux et son étude fait depuis peu l’objet de recherches visant à approfondir les connaissances relatives à ce processus. Ce travail de thèse cherche (i) à caractériser la prédation des graines d’adventices, les principaux prédateurs Carabidæ et la ressource en graines disponible à l’échelle locale dans une culture courante (blé d’hiver); (ii) à étudier précisément les profils de prédation des principaux prédateurs et les interactions entre les composantes biologiques impliquées; (iii) à introduire des éléments de réponse relatifs au potentiel de régulation des communautés d’adventices via la prédation des graines par les Carabidæ. Des approches complémentaires ont été utilisées afin de répondre à ces problématiques : un suivi à long terme de terrain, des tests de préférences en laboratoire, une simulation des taux de prédation à long terme à partir des données ponctuelles ainsi qu’une étude à grande échelle des prédateurs et du stock de graines.L’étude des variations spatio-temporelles de la prédation via un dispositif de terrain durant la période d’activité des prédateurs a mis en évidence trois pics de prédation dont un seul correspond au pic de prédateurs (avant la moisson). La ressource en graines disponible au sol est quant à elle présente majoritairement lors du premier et du dernier pic de prédation, et aucune augmentation de ressource n’a été observée après moisson. Ces dynamiques semblent stables, restant valables indépendamment de l’échelle spatiale (intra ou interchamp) et des espèces carabiques et adventices étudiées.Toutes les espèces adventices ne font pas l’objet de la même intensité de prédation, et de manière générale, les graines de petites tailles ont été préférentiellement prédatées, au champ comme en test de cafétéria au laboratoire. Cependant, les espèces carabiques semblent avoir des profils de prédation différents entre guildes trophiques, ainsi qu’au sein d’une même guilde. De ce fait, la prise en compte des préférences de consommation dans l’étude des relations prédation-prédateurs tout comme la combinaison des données prédateurs et graines disponibles permet parfois d’améliorer les corrélations, notamment pour les espèces les plus prédatées.Une simulation de la prédation annuelle suggère des pertes en graines dues à la prédation non négligeables, pouvant atteindre pour l’espèce la plus prédatée, ici Viola arvensis, jusqu’à près de 80% des graines disponibles. En parallèle, une étude à grande échelle de l’évolution du stock de graines montre une corrélation négative entre prédateurs et évolution de la banque de graines, suggérant une régulation de la banque de graines via les prédateurs carabiques.L’ensemble de ces résultats suggère que prendre en compte la diversité fonctionnelle des communautés de prédateurs et d’adventices est un point important dans la compréhension de la prédation compte tenu des préférences de consommation des prédateurs et des dynamiques temporelles des différents acteurs. / Agroecology gives evidence of new perspectives in agriculture, and open doors for alternative weed management approaches through different regulation mechanisms. Seed predation is one of them, and the interest is growing to deepen knowledge, relative to this process. This Phd work aims (i) to describe weed seed predation, the dominant carabid predators and the available resource at a local scale in a common crop (winter wheat); (ii) to study predation profiles of main predators, and the pair-wise correlations between the biological components of the system; (iii) to bring new insights regarding potential regulation of weed communities, through seed predation by carabid beetles. Complementary approaches have been used to tackle these aspects: a long-term field study, some cafeteria tests, a simulation of annual predation rates from point-to-point estimates, as well as a large-scale field study of predators and seed resource. Study of spatio-temporal variations of predation, via field experiment during the main activity period of carabids, has shown a three-peak pattern, one of them corresponding to predators’ peak, just before harvest. Weed resource available on soil surface is high in the first and last peaks of predation, and no increase of resource has been observed after harvest. These dynamics are independent of the spatial scale (intra or inter-field) and carabid species. The different weed species do not show the same levels of predation, and, as a whole, small-seeded species are more eaten, in both lab and field conditions. However, carabids have different preferences among trophic guilds, but also within a same guild. Therefore, in order to study predation, it is essential to combine predators and seed data, as well as considering preferences of predators. A simulation of annual seed predation shows important rates of seed loss, reaching up to 80% for the most predated species, V.arvensis. A large scale study of seed bank shows a negative correlation between predators’ activity density and seed bank change, assuming that there is a seed bank regulation by carabid predators. All together, these results show that functional diversity of predators’ and weeds’ communities is a key factor in understanding predation.