Fran├žais
image
In the field of systems biology, the "formal bioinfo" project aims to provide rigorous and formal frameworks for modeling complex dynamic biological systems. The group focuses on the formalisation of behavior of such systems, on the analysis of models, and on the identification of the environment, of interactions and of timing constraints to make the proposed models consistent with observation.
  • Methodological approach A model should evolve to reflect the evolution of knowledge about the biological system it represents. To avoid to repeat the entire modeling process as soon as a new information contests the model, it is necessary to handle, at every stage, not only a single model of the biological system but all possible formalisations consistent with biological knowledge. Thus, a new knowledge represents only an additional constraint on the set of models.

    To accelerate the process of refining a model, we seek to optimize the selection of biological experiments to implement in order to converge as quickly as possible to predictive modeling. The task is arduous because of observability constraints (not all system variables are observable) and operability constraints (some initial states can not be chosen). Formal models can help in the selection of the most discriminating experiences.

  • Verification of behavioral properties Verification of behavioral properties is fundamental to verify the consistency of the built models with respect to known properties. The group has developped a first tool SMBioNet that automatically retrieves, through intensive model checking, all the settings of a gene regulatory graph leading to a behaviour consistent with the knowledge/assumption, expressed via temporal logic formulae, about the system dynamics. The DyMBioNet modeling environment includes SMBioNet but adds a simulator and fair model-checking.
    We have also developed an approach based on the Hoare logic and the calculation of the lowest precondition to generate the constraints on the values of the parameters. The observed behavior specifications play a role similar to that of the programs in the classical Hoare logic, and the lower precondition characterizes the compatible settings, expressed as constraints on the parameters.

  • Chronometric information Chronometric information (which completes the knowledge on the sequence of events by adding temporal information on actions) are often easy to obtain from experiments but rarely used. Chronometric information includes the time required for the system to change state, or the time mandatory to go through a sequence (path) of states and observe the complete transformation. They could be used to constrain the parameterization of models, thus we are developing hybrid formal models for biological systems in which one can formally manipulate such chronometric information.

    Recently, we developed a Hoare logic for these hybrid systems in order to build the constraints on the parameters of the model compatible with the observed traces. Holmes BioNet implements these ideas and uses the constraints solver AbSolute to produce solutions.

"Formal Bioinfo" is a research group from I3S, a joint research centre of university of Nice and CNRS.

Scientific events

type: mini-workshop
place: Sophia-Antipolis
date: 12th november 2019
type: CNRS thematic school
place: Ile de Porquerolles
date: 23-28 june 2019
type: CNRS thematic school
place: Ile de Porquerolles
date: 6-10 june 2016
type: Workshop I3S
place: Nice
date: 4-7 november 2014
type: CNRS thematic school
place: Ile de Porquerolles
date: 24-28 june 2013
type: CNRS thematic school
place: Ile de Porquerolles
date: 6-11 june 2010
type: Thematic Research School
lieu: Evry
date: du 19 au 23 mars 2018
type: Thematic Research School
lieu: Lyon
date: du 13 au 17 mars 2017
type: Thematic Research School
lieu: Evry
date: du 21 au 25 mars 2016
type: Thematic Research School
lieu: Strasbourg
date: du 23 au 27 mars 2015
type: Thematic Research School
lieu: Evry
date: du 24 au 28 mars 2014
type: Thematic Research School
lieu: Evry
date: du 25 au 29 mars 2013