Jeudi 16 janvier 2002
14h00 - 15h00

Comment valider un modèle mathématique en biologie?

Janine GUESPIN-MICHEL
Professeur Emérite
Laboratoire de Microbiologie du Froid
Université de Rouen

Les infections par la bactérie, généralement inoffensive, Pseudomonas aeruginosa, peuvent être mortelles chez des malades atteints de mucoviscidose. Il existe un consensus chez les spécialistes, selon lequel les causes de cette létalité reposent sur une mutation sélectionnée dans les poumons malades. Il existe cependant une autre hypothèse, celle d'une modification épigénétique, qui, si elle était vraie, conduirait à une modification profonde de la thérapeutique. Cette hypothèse s'appuie sur un modèle mathématique, construit à partir des réseaux de régulation mis en évidence par les méthodes de la génétique moléculaire.
Il est clair qu'une validation expérimentale est indispensable.
Une approche informatique, basée sur les notions d'observabilité et d'opérabilité a été proposée et a permis de montrer dans quelles conditions une expérience "clef", suggérée par les biologistes, est susceptible de falsifier ou de valider l'hypothèse proposée. Cette approche est largement inspirée de travaux antérieurs sur la génération de tests de logiciels à partir de spécifications formelles.

Vendredi 17 janvier 2002
9h15 - 10h15

La méthode B et l'ingénierie système

Didier ESSAMÉ, PhD
Formal Methods Engineer
B, UML & UPM
Siemens Transportation Systems
Montrouge

L'intérêt de la méthode B pour les études systèmes n'est plus à démontrer, mais il reste à intégrer une telle approche dans un contexte industriel Nos travaux s'inscrivent dans le cadre du projet de recherche PREDIT mené en collaboration avec la RATP sous la tutelle du Ministère des Transports. Dans le cadre de ce projet, nous avons défini par rapport aux principaux processus de l'ingénierie système, un ensemble d'activités dans lesquelles la formalisation et en particulier la méthode B peut être appliquée. Ces activités ont été découpées de façon à pouvoir introduire progressivement l'utilisation de la méthode formelle B dans les études systèmes. En s'appuyant sur les processus d'ingénierie définis par les normes IEEE 1220 et EIA 632, le projet PREDIT a permis d'identifier des activités de l'ingénierie système où la formalisation B est d'un intérêt certain. Les activités suivantes ont été retenues :

• définir les concepts significatifs du système;
• définir le système du point de vue de ses utilisateurs (définition du besoin) ;
• définir le système du point de vue de ses concepteurs (définition des exigences) ;
• définir les fonctions du système et leur allouer des exigences (analyse comportementale).

Un volet formel a été introduit dans chacune de ces activités dans le but respectivement :

• d'exprimer les propriétés, les contraintes et les hypothèses sur les concepts du système ;
• de lever les non-dits et les ambiguïtés dans l'expression du besoin ;
• de vérifier par la preuve que les choix techniques (expression des exigences) correspondent bien aux besoins des utilisateurs ;
• de vérifier par la preuve que l'allocation des exigences ne contredit ni les exigences, ni le besoin.

Pour chacune de ces activités, des techniques d'utilisation et d'application précises de la méthode B ont été définies afin de favoriser une utilisation systématique.
Dans cet exposé nous présentons des éléments méthodologiques relatifs à ces techniques.