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.