Des mesures de l'activité du cerveau humain peuvent être obtenues par diverses techniques d'imagerie neuro-fonctionnelle. Dans le domaine des neurosciences, les études menées grâce à ces nouvelles techniques sont appelées études d'activation. Elles mettent en évidence l'organisation en réseau des aires cérébrales mises en jeux lors de la réalisation de tâches cognitives particulières. La complexité du traitement de l'information cérébrale et l'incomplétude de l'observation rendent difficile l'interprétation de ce fonctionnement et rendent nécessaire la construction d'un outil de modélisation et de simulation. La nécessité de comprendre l'organisation fonctionnelle du cerveau humain, nous impose en plus de recourir à des formalismes permettant d'en avoir une représentation explicite. Dans cette optique, nous proposons un formalisme original, basé sur des graphes d'influences causales et une représentation qualitative de l'information. Les graphes d'influences sont tout à fait appropriés à la représentation de la double organisation du cerveau, en réseaux anatomiques (structurels) et fonctionnels. L'originalité de notre approche est double. D'une part, nous proposons une architecture hiérarchique fondée sur la notion de composant et qui permet de réduire la complexité des modèles tout en augmentant leur réutilisabilité. D'autre part, nous utilisons un formalisme unique pour décrire les niveaux structurels et fonctionnels cérébraux. La modélisation explicite de l'information cérébrale nous a conduit à proposer une représentation qualitative mixte, sous la forme de couples (intervalle, symbole). Ceci permet à la fois de prendre en compte l'amplitude de cette information, bruitée par les techniques d'imagerie, et sa catégorie. Nous proposons le simulateur BIOCAEN, fondé sur le formalisme ci-dessus. La simulation consiste en la propagation des influences à chaque instant d'une horloge discrète. Ce mécanisme permet de prendre en compte les processus automatiques qui constituent la majeure partie du fonctionnement cérébral. La contribution de notre travail à l'exploration du fonctionnement du cerveau humain réside dans la mise à disposition des chercheurs en neurosciences, d'un formalisme permettant d'exprimer explicitement, à un haut niveau d'abstraction, les hypothèses sur la propagation de l'information cérébrale et d'un simulateur permettant de les mettre en œuvre. Les hypothèses sont décrites dans des modèles où l'architecture causale offre un support à l'expression des réseaux anatomiques d'aires cérébrales, chacune d'entre elles étant représentée par un sous-réseau fonctionnel de processeurs d'information. La validation des hypothèses est réalisée par la confrontation des résultats de la simulation du modèle par BIOCAEN aux données de l'imagerie neuro-fonctionnelle.

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 systèmes hybrides sont au cœur des systèmes cyber-physiques. De tels systèmes représentent l’interaction de processus physiques continus modélisant généralement l'environnement avec des décisions discrètes issues d'un système de contrôle commande électronique. La vérification de ces systèmes est cruciale pour assurer leur sûreté dès la phase de modélisation. Les recherches sur les systèmes hybrides ont de nombreux domaines d’application, notamment le transport, l’aéronautique et la biologie. La thèse étudie des principes du raisonnement qualitatif et les applique à la vérification des systèmes hybrides. Le travail consiste à élaborer une méthode pour abstraire le système hybride en utilisant des principes qualitatifs. On recourt à une discrétisation finie de l'espace d'état tout en conservant des caractéristiques qualitatives du système. L'abstraction calculée permet de prouver des propriétés au niveau du système hybride concret et fournit une représentation du comportement global du système. Un outil développé en C++ permet de calculer l'abstraction d'un système hybride donné. Une évaluation de ses performances est établie. On s'intéresse particulièrement à une propriété de sûreté des systèmes appelée diagnosticabilité. Un modèle de système est dit diagnosticable s'il permet d'identifier sans ambiguïté la survenue de toute faute modélisée à partir des seules observations disponibles du système jusqu’à un certain délai après l’occurrence de la faute. Une méthode qui consiste à utiliser l'abstraction établie précédemment pour vérifier la diagnosticabilité d'un système hybride est proposée. / Hybrid systems are at the core of cyber-physical systems. Such systems represent the interaction between continuous physical processes generally modelling the environment with discrete decisions from control electronic signaling. The verification of these systems is crucial to ensure safety at the modeling stage. The application of hybrid systems is present in many fields such as transportation, biology and avionics. The thesis studies principals from the qualitative reasoning domain and applies them to the verification of hybrid systems. The accomplished work elaborates methods to abstract a hybrid system using qualitative principles. These methods consist in discretizing the state space to a finite number of states while conserving qualitative characteristics. The computed abstraction allows to prove properties at the level of the concrete hybrid system and presents a representation of the global behavior of the system. A tool developed in C++ computes the abstraction of a given hybrid system. An evaluation of its performance is performed. We are also interested in a particular property called diagnosability. The system is said to be diagnosable when it is capable to identify modeled faults using limited specified observations. A method that uses the computed abstraction to verify diagnosability of a given hybrid system is proposed.

Les réseaux de régulation génique contrôlent le développement et le fonctionnement des organismes vivants. Etant donné que la plupart des réseaux de régulation génique d'intérêt biologique sont grands et que leur dynamique est complexe, la compréhension de leur fonctionnement est un problème biologique majeur. De nombreuses méthodes ont été développées pour la modélisation et la simulation de ces systèmes. Etonnamment, le problème de la validation de modèle n'a reçu jusqu'à récemment que peu d'attention. Pourtant, cette étape est d'autant plus importante que dans le contexte de la modélisation de réseaux de régulation génique, les systèmes modélisés sont complexes et encore imparfaitement connus.<br /><br />Dans cette thèse, nous proposons une approche permettant de tester la validité de modèles de réseaux de régulation génique en comparant les prédictions obtenues avec les données expérimentales. Plus spécifiquement, nous considérons dans ce travail une classe de modèles qualitatifs définis en termes d'équations différentielles linéaires par morceaux (LPM). Ces modèles permettent de capturer les aspects essentiels des régulations géniques, tout en ayant une forme mathématique simple qui facilite leur analyse symbolique. Egalement, nous souhaitons utiliser les informations qualitatives sur la dynamique du système données par les changements du sens de variation des concentrations des protéines du réseau. Ces informations peuvent être obtenues expérimentalement à partir de profils d'expression temporels.<br /><br />La méthode proposée doit satisfaire deux contraintes. Premièrement, elle doit permettre d'obtenir des prédictions bien adaptées à la comparaison avec le type de données considéré. Deuxièmement, étant donné la taille et la complexité des réseaux d'intérêt biologique, la méthode doit également permettre de vérifier efficacement la cohérence entre prédictions et observations.<br /><br />Pour répondre à ces deux contraintes, nous étendons dans deux directions une approche précédemment développée par de Jong et collègues pour l'analyse symbolique des modèles LPM qualitatifs. Premièrement, nous proposons d'utiliser une représentation plus fine de l'état du système, permettant d'obtenir, par abstraction discrète, des prédictions mieux adaptées à la comparaison avec les données expérimentales. Deuxièmement, nous proposons de combiner cette méthode avec des techniques de model checking. Nous montrons que l'utilisation combinée d'abstraction discrète et de model checking permet de vérifier efficacement les propriétés dynamiques, exprimées en logique temporelle, des modèles continus.<br /><br />Cette méthode a été implémentée dans une nouvelle version de l'outil Genetic Network Analyzer (GNA 6.0). GNA 6.0 a été utilisé pour la validation de deux modèles grands et complexes de l'initiation de la sporulation chez <I>B. subtilis</I> et de la réponse au stress nutritionnel chez <I>E. coli</I>. Nous avons ainsi pu vérifier que les prédictions obtenues étaient en accord avec la plupart des données expérimentales disponibles dans la littérature. Plusieurs incohérences ont également été identifiées, suggérant des révisions des modèles ou la réalisation d'expériences complémentaires. En dehors d'une contribution à une meilleure compréhension du fonctionnement de ces systèmes, ces deux études de cas illustrent plus généralement que, par la méthode proposée, il est possible de tester si des prédictions obtenues pour des modèles complexes sont cohérentes avec un large éventail de propriétés observables expérimentalement.

Inventer des circuits de l'électronique de puissance est une activité intellectuelle qui met en jeu de nombreuses connaissances, requiert du savoir-faire et de la créativité. L'objectif de cette thèse est de concevoir un système informatique simulant cette activité. A cet effet, un système constitué de deux modules a été implanté. Le premier propose les circuits qui ne présentent pas de grossier défaut de conception, au terme d'une recherche heuristique dans un espace organisé en hiérarchie d'abstractions. Cette organisation particulière des connaissances permet de focaliser, aussi tôt que possible, la recherche sur les circuits potentiellement intéressants. Pour éviter que ce module engendre des doublons, la représentation par graphes de liens a été utilisée. Cette mise en (\oe)uvre a donné lieu à un algorithme qui, contrairement à ceux qui ont été décrits dans la littérature, transforme un circuit en un graphe de liens parfaitement adapté au formalisme. Le second module analyse qualitativement le fonctionnement des circuits ainsi engendrés. Il décrit notamment leur fonctionnement dans des termes identiques à ceux employés par les ingénieurs. Il permet ainsi d'exprimer intuitivement les critères imposés par un cahier des charges et de sélectionner les circuits qui le vérifient. L'approche proposée est viable car le système a redécouvert les principaux représentants de classes importantes de circuits. Il a également proposé de circuits nouveaux aux performances a priori comparables à celles des circuits connus. Le système présenté dans cette thèse permet ainsi d'envisager une étude rationnelle des dispositifs de l'électronique de puissance. Plus généralement, il prouve l'efficacité des techniques d'intelligence artificielle sur un domaine concret et met en évidence l'intérêt de l'utilisation des abstractions pour la résolution de problème.

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.

Le logiciel embarqué est devenuaujourd’hui incontournable dans la plupart dessecteurs industriels. Ce dernier fait appel engénéral à des connaissances métier différentes.L’ensemble du système (le logiciel et sonenvironnement) est ainsi spécifié d’une manièrehétérogène, avec des parties discrètes et d’autrescontinues. La simulation de ces systèmeshybrides nécessite des données précises et unesynchronisation des changements continus avecles transitions discrètes. Mais, dans les premièresphases de conception, l’absence des informationsempêche de simuler le système numériquement.Dans notre thèse, nous présentons un nouveaulangage qualitatif dédié à la simulationqualitative des systèmes hybrides. Ce nouveaulangage consiste à modéliser les relations entreles variables du système. Il est implémenté dansDiversity, un moteur d’exécution symbolique,pour construire les traces du système. Nousavons appliqué cette approche à l’analyse desmodèles SysML, en utilisant une transformationM2M à partir de SysML vers un langage pivot,une transformation M2T à partir de ce langagevers Diversity. Nous avons aussi analysé lestraces brutes de l’exécution symbolique deDiversity pour construire les comportementsqualitatifs du système. / Embedded software has becomeessential in most industrial sectors. The latterusually involves various business knowledge.The whole system (the software and itsenvironment) is specified in a heterogeneousform, with discrete and continuous parts.Simulating these hybrid systems requiresprecise data and synchronization of continuouschanges and discrete transitions. However, inthe first design steps, missing informationforbids numerical simulation. We present in ourthesis a new qualitative language for qualitativesimulation of hybrid systems, which consists incomputing the relationships between the systemvariables. This language is implemented in theDiversity symbolic execution engine to build thetraces of the system. We apply this approach tothe analysis of SysML models, using an M2Mtransformation from SysML to a pivot language,an M2T transformation from this language toDiversity. We also analyze the brutal symbolictraces obtained by Diversity to build the realqualitative behaviors of the system.

Les modèles de la biologie des systèmes visent à comprendre le comportement d’une cellule à travers un réseau biomoléculaire complexe. Dans a littérature, la plupart des études ne se sont intéressés qu’à la modélisation des parties isolées du réseau biomoléculaire com les réseaux métaboliques, etc. Cependant, pour bien comprendre le comportement d’une cellule, nous devons modéliser et analyser le réseau biomoléculaire dans son ensemble. Les approches existantes ne répondent pas suffisamment à ces exigences. Dans ce projet de recherche,nous proposons une plate-forme qui permet aux biologistes de simuler les changements d’état des réseaux biomoléculaires dans le but de piloter leurs comportements et de les faire évoluer d’un état non désiré vers un état souhaitable. Cette plate-forme utilise des règles, des connaissances et de l’expérience, un peu comme celles que pourrait en tirer un biologiste expert. La plate-forme comprend quatre modules : un module de modélisation logique, un module de modélisation sémantique, un module de simulation qualitative à événements discrets etun module d’optimisation. Dans ce but, nous présentons d’abord une approche logique pour la modélisation des réseaux biomoléculaires complexes, incluant leurs aspects structurels, fonctionnels et comportementaux. Ensuite, nous proposons une approche sémantique basée sur quatre ontologies pour fournir une description riche des réseaux biomoléculaires et de leurs changements d’état. Ensuite, nous présentons une méthode de simulation qualitative à événements discrets pour simuler le comportement du réseau biomoléculaire dans le temps. Enfin, nous proposons une méthode d’optimisation multi-objectifs pour optimiser la transitabilité des réseaux biomoléculaires complexes dans laquelle nous prenons en compte différents critères tels que la minimisation du nombre de stimuli externes, la minimisation du coût de ces stimuli, la minimisation du nombre de noeuds cibles et la minimisation de l’inconfort du patient. En se fondant sur ces quatre contributions, un prototype appelé CBN-Simulateur a été développé. Nous décrivons nos approches et montrons leurs applications sur des études de cas réels, le bactériophage T4 gene 32, le phage lambda et le réseau de signalisation p53. Les résultats montrent que ces approches fournissent les éléments nécessaires pour modéliser, raisonner et analyser le comportement dynamique et les états de transition des réseaux biomoléculaires complexes. / Systems biology models aim to understand the behaviour of a cell trough a complex biomolecular network. In the literature, most research focuses on modelling isolated parts of this network, such as metabolic networks.However, to fully understand the cell’s behaviour we should analyze the biomolecular network as a whole. Avail-able approaches do not address these requirements sufficiently. In this context, we aim at developing a platform that enables biologists to simulate the state changes of biomolecular networks with the goal of steering their be-haviours. The platform employs rules, knowledge and experience, much like those that an expert biologist mightderive. This platform consists of four modules: a logic-based modelling module, a semantic modelling module,a qualitative discrete-event simulation module and an optimization module. For this purpose, we first present alogic-based approach for modelling complex biomolecular networks including the structural, functional and be-havioural aspects. Next, we propose a semantic approach based on four ontologies to provide a rich description of biomolecular networks and their state changes. Then, we present a method of qualitative discrete-event simulation to simulate the biomolecular network behaviour over time. Finally, we propose a multi-objective optimization method for optimizing the transittability of complex biomolecular networks in which we take into account various criteria such as minimizing the number of external stimuli, minimizing the cost of these stimuli, minimizing the number of target nodes and minimizing patient discomfort. Based on these four contributions, a prototype called the CBNSimulator was developed. We describe our approaches and show their applicability through real cases studies, the bacteriophage T4 gene 32, the phage lambda, and the p53 signaling network. Results demonstrate that these approaches provide the necessary elements to model, reason and analyse the dynamic behaviour and the transition states of complex biomolecular networks.

La thèse est que la représentation par contraintes, en terme de langage et la déduction par la gestion automatique des réseaux de contraintes est une voie adéquate pour les systèmes d'aide à la conception en ingénierie. Deux techniques de l'Intelligence Artificielle à savoir la Propagation de Contraintes et le Raisonnement Qualitatif sont abordées. La Propagation de Contraintes est un mécanisme d'inférences déductives sur les réseaux de contraintes. Ce mécanisme présente plusieurs difficultés, particulièrement dans les calculs pas-à-pas de la résolution des relations entre valeurs des variables. Pour améliorer ce mécanisme, il est proposé dans le présente travail des algorithmes de filtrage sur la consistance locale dans des réseaux de contraintes algébriques n-aires. Ainsi, le concept de réseaux dynamiques est exploité comme un module d'aide à la conception. Le Raisonnement Qualitatif permet aux concepteurs d'analyser les modèles quand la connaissance est incomplète. L'approche de la Simulation Qualitative est proposée. L'adéquation de celle-ci est illustrée par d'une part, la représentation de connaissances incomplètes en termes de contraintes qualitatives, et d'autre part, sa capacité de saisir les comportements qualitatifs possibles des modèles. Un ensemble de logiciels est développé et leur efficacité démontrée sur des cas simples.