Méthodes de vérification formelle pour la modélisation en biologie: le cas des réseaux de régulation biologique

On ne compte plus le nombre de fois où les chercheurs en méthodes formelles pour le génie logiciel ont entendu cette plaisanterie : « Les méthodesformelles ont toujours été l'avenir de l'informatique... et le resteront toujours ! ». Dans ce chapitre nous montrons que les méthodes formelles sont le présent de l'analyse des réseaux de régulation en biologie des systèmes. Plus précisément, nous donnons les définitions symboliques de deux formalismes : celui de la théorie qualitative de modélisation des réseaux de régulation biologique de René Thomas, et celui de la modélisation hybride, avec délais, de ces réseaux. Nous décrivons pour chacun des deux formalismes une méthodologie complète d'aide à la modélisation fondée sur les méthodes de vérification formelle. On se focalise sur une adaptation aux réseaux de régulation des techniques de validation par model-checking et de preuve en logique de Hoare, mais bien d'autres méthodes formelles sont applicables en modélisation pour la biologie. Nous montrons ainsi que 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.