- Approche méthodologique
Un modèle d'un système biologique n'est pas statique et doit évoluer
afin de refléter l'évolution des connaissances sur le système.
Pour éviter de relancer le processus entier de modélisation dès qu'une
nouvelle information remet en question le modèle, il est souhaitable de
maintenir, à chaque étape, non pas un modèle unique du système
biologique, mais toutes les formalisations possibles compatibles avec
les connaissances biologiques. Ainsi, une connaissance nouvelle n'est
plus qu'une contrainte supplémentaire sur l'ensemble des modèles.
Pour accélérer le processus de raffinement d'un modèle, nous cherchons à optimiser la sélection des expériences biologiques à réaliser afin de converger le plus rapidement possible vers des modélisations prédictives. La tâche est ardue en raison des contraintes observationnelles (les variables du système ne sont pas toutes observables) et des contraintes d'opérabilité (certains états initiaux ne peuvent pas être choisis). Les modèles formels peuvent aider à la sélection des expériences les plus discriminantes.
- Vérification de propriétés comportementales
La vérification des propriétés dynamiques est indispensable car elle
permet de vérifier la cohérence des modèles construits vis-à-vis de
propriétés connues. Nous avons développé un premier environnement de
modélisation formelle SMBioNet qui permet de sélectionner
automatiquement, à travers un usage intensif du model-checking, tous
les paramétrages d'un graphe de régulation génique qui mènent à un
comportement cohérent avec les connaissances ou hypothèses faites sur
la dynamique du système, ces connaissances ou hypothèses étant
exprimées dans un langage de logique temporelle. L'environnement de
modélisation DyMBioNet inclut SMBioNet en y ajoutant un simulateur
ainsi que du model-checking équitable.
Nous avons également développé une approche basée sur la logique de Hoare et sur le calcul de la plus faible précondition pour générer les contraintes sur les valeurs des paramètres. Les spécifications du comportement observé jouent un rôle similaire à celui des programmes dans la logique de Hoare classique, et la plus faible précondition caractérise les paramétrages compatibles, exprimées comme des contraintes sur les paramètres. - Informations chronométriques
Les informations chronométriques (qui complètent la chronologie des
événements en ajoutant des informations temporelles sur la durée des
actions) sont souvent faciles à obtenir expérimentalement, mais
rarement utilisées. Par exemple il peut être facile de connaître le
temps nécessaire au système pour passer d'un état à son successeur ou
bien pour passer d'un état à un autre à travers un chemin. Ces durées
pourraient être utilisées pour contraindre les paramétrages
admissibles. Nous développons donc des modèles formels hybrides pour
les systèmes biologiques dans lesquels on peut manipuler formellement
cette information chronométrique.
Récemment, nous avons développé une logique de Hoare pour ces systèmes hybrides afin de construire les contraintes sur les paramètres du modèle qui le rendent compatible avec les traces observées. Holmes BioNet implémente ces idées et utilise le solveur de contraintes AbSolute pour exhiber des solutions.