Search

Ce chapitre démontre que la modélisation des réseaux de régulation biologiques est grandement facilitée par des méthodes symboliques de vérification formelle comme le model-checking et les preuves en logique de Hoare. Il présente une méthodologie complète de modélisation formelle où les approches logiques classiques du génie logiciel s'adaptent remarquablement efficacement au problème majeur de la modélisation des systèmes complexes: l'identification des paramètres.

Adaptation of metabolism is a response of many eukaryotic cells to nutrient heterogeneity in the cell microenvironment. One of these adaptations is the shift from respiratory to fermentative metabolism, also called the Warburg/Crabtree effect. It is a response to a very high nutrient increase in the cell microenvironment, even in the presence of oxygen. Understanding whether this metabolic transition can result from basic regulation signals between components of the central carbon metabolism are the the core question of this work. We use an extension of the René Thomas modeling framework for representing the regulations between the main catabolic and anabolic pathways of eukaryotic cells, and formal methods for confronting models with known biological properties in different microenvironments. The formal model of the regulation of eukaryote metabolism defined and validated here reveals the conditions under which this metabolic phenotype switch occurs. It clearly proves that currently known regulating signals within the main components of central carbon metabolism can be sufficient to bring out the Warburg/Crabtree effect. Moreover, this model offers a general perspective of the regulation of the central carbon metabolism that can be used to study other biological questions.

International audience; When designing a biological regulatory network, new information or wet experiments can require adding variables or interactions, inside a previously validated model. They can result in complete reconsiderations of established behaviours. Fortunately, formal methods allow for fully automated verification of properties, and TotemBioNet is an efficient software integrating a collection of formal approaches for regulatory networks. It allowed us to develop a multidisciplinary methodology for designing large dynamical models in an incremental way, including non regression proofs (preservation of important biological properties).

TotemBioNet is a new software platform to assist the design of qualitative regulatory network models by combining “genetically modified Hoare logic”, temporal logic model checking and optimized enumeration techniques. TotemBioNet is particularly efficient to manage parameter identification, the most critical step of formal modelling. It is also remarkably flexible and efficient to check properties in order to explore biological assumptions. To illustrate this efficacy, we address the classical example of the cell cycle, where the passage from one phase to the next one, called checkpoint, is crucial but is usually a rather fuzzy informal concept. The cyclic behaviour of the cell cycle is specified by temporal logic and the order of individual events inside each phase is explored thanks to quantifiers introduced in Hoare logic. This way, TotemBioNet rapidly suggests a sensible formalization of the notion of checkpoint.

International audience