PhD Defense of Alexandre Rocca on 05/07/2018

PhD Defence of Alexandre ROCCA from BCM team on 2018/07/05 at 1:30pm :
 

“ Formal methods for modelling and validation of biological models ”

 

Supervision:

- Mme Thao Dang, Directrice de Recherche CNRS, laboratoire Verimag , Grenoble Directeur
- M. Eric Fanchon, Chargé de Recherche Université Grenoble Alpes, laboratoire TIMC-IMAG, Grenoble CoDirecteur

Jury :
- Pr François Fages, Directeur de Recherche à l’INRIA Saclay, Rapporteur
- Pr Ovidiu Radulescu, Professeur, DIMNP Université de Montpellier 2, Rapporteur
- Pr Hidde de Jong, Directeur de Recherche à l’INRIA Montbonnot, Examinateur
- Dr David Safranek, Professeur Assistant à l’Université de Masaryk, Département "Machine Learning and Data Processing", République Tchèque , Examinateur

 

Place :
Auditorium du bâtiment IMAG, Université Grenoble Alpes, 700 Avenue centrale, 38401 Saint Martin d’Hères

 

*****

Key-words :

Reachability analysis, multi-scales systems, biological systems, modelisation

Abstract :

The focus of this thesis is the modelling and analysis of biological systems using formal methods. The dynamics of biological systems exhibit continuous behaviours but also abrupt changes.
Ordinary differential equations and hybrid dynamical systems are two mathematical formalisms that naturally model such dynamics. A crucial aspect of modelling is the determination of valid parameter values that enable to simulate the behaviour and reproduce experimental data sets. If no valid parameter values are found it becomes necessary to revise the model. An option is to replace one or several lumped parameters (parameters which represent a set of processes) by functions of time.

In this thesis, we first study the model revision problem on hybrid dynamical systems. To this aim, we propose a greedy scheme of optimal control methods based on occupation measures and convex relaxations. Then, we study how to characterize dynamical properties of a model using set-based simulations and reachability analysis. For this purpose, we propose two methods : the first one, which relies on Bernstein expansion, is an extension for hybrid dynamical systems of the reachability tool Sapo, while the other one uses Krivine-Stengle representations to perform the reachability analysis of polynomial ODEs.
Finally, we also propose a methodology to generate hybrid dynamical systems modelling a class of experimental protocols.

The proposed methods are applied to different case studies. We first propose a model of haemoglobin production during the differentiation of an erythrocyte in the bone marrow. To develop this model, we first apply the Monte-Carlo based parameters synthesis, followed by the model revision to correctly reproduce the experimental data. We also propose a preliminary study of the effect of low dose Cadmium on glucose response at different steps of a rat growth. Finally, we apply the reachability analysis techniques for the validation on large parameters set of the existing iron homoeostasis model. We note the haemoglobin production process, as well as the glucose response system can be formalised within their experimental context as hybrid dynamical systems. Thus, they serve as proof of concept for the methodology of biological experimental protocols modelling.