=======================================================================
Club SEE "Systèmes Informatiques de Confiance"
http://www.rennes.supelec.fr/sic/
========================================================================
Reunion du 19 juin 2003 à l'ENST (Paris)
Thème : "Méthodes formelles"
========================================================================
- 10h00-10h45 Randim Famanta "Méthodes formelles pour la vérification de
logiciels avioniques" - Intervention annulée.
L'évolution des exigences sur les logiciels avioniques combinée avec
les difficultés croissantes pour la mise en oeuvre des techniques de
vérification par exécution ont motivé la recherche et le développement
de nouvelles solutions: les techniques formelles de vérification de
propriétés dynamiques par analyse statique. Cet exposé présente la
démarche entreprise à Airbus France qui a abouti notamment à une
première mise en oeuvre sur le programme A380.
- 10h45-11h30 Jean-Louis Lanet "Utilisation de techniques formelles
pour les cartes à puces" [pdf]
La carte à puce est domaine où l'utilisation de méthodes formelles
semble idéal. En effet, trois besoins sont clairement identifiés :
gérer la complexité des nouveaux OS embarqués, certification à un haut
niveaux des cartes et réduire le coût du processus de qualification.
Nous avons démontré précédemment que lutilisation de méthodes
formelles était techniquement faisable, il nous reste à démontrer
quelle est économiquement viable. Pour ce faire nous avons réalisé
deux expériences Matisse et Jack que nous présentons dans cet exposé.
Auparavant nous ferons une présentation des différentes utilisations
des méthodes formelles pour ce domaine.
- 11h30-12h15 Jean-Raymond Abrial "Construction et validation formelle
de protocoles-réseau avec B" [pdf], [Développement en B]
On montre comment s'y prendre pour construire et prouver des
protocoles par raffinements successifs en "B-événementiel".
- 12h15 - 13H45 : Pause déjeuner
- 13h45- 14h30 Georges Mariano "Projet de développement d'outils libres
pour B (BRILLANT)" [pdf]
- 14h30- 15h15 Jean-Louis Boulanger "B-HDL : Conception sûre de circuit" [pdf]
B-HDL (http://www.hds.utc.fr/bhdl/) est un projet qui vise à permettre
la conception sûre de circuit au travers d'un couplage entre la méthode B
et le langage VHDL.
Il existe de nombreux environnements permettant de manipuler des
modèles VHDL, mais notre approche vise a apporter un complément au
travers de la notion de preuve de propriété (Safety, Liveness, ..). Ce
couplage est réalisé au travers d'un processus de traduction, en cour
d'outillage qui permet de traduire un modèle VHDL en un modèle B.
Ces travaux sont réalisés par l'UTC-Heudiasyc (Univ. de Technologie de
Compiègne, le LIFL (Univ. de Lille) et l'ESTAS (INRETS)
- 15h15- 16h00 Gilles Bernot & Jean-Paul Comet « Logique temporelle et
Model-Checking pour les réseaux de régulation biologiques » [pdf]
Les réseaux de régulation biologiques permettent, entre autres, de
modéliser les interactions entre les gènes dans une cellule. À la
suite du séquençage de nombreux génomes, dont le génome humain, la «
postgénomique » en biologie a pour but de trouver les gènes, leurs
fonctions et leurs interactions. Les réseaux de régulation prennent
ici une importance majeure et une difficulté importante est le «
passage à l'échelle » : mettre au point des modèles à partir des
données biologiques et prédire les comportements du système.
Cet exposé présente une théorie discrète des réseaux de régulation
inspirée des travaux du biologiste René Thomas à Bruxelles. Nous
proposons une formalisation (au sens informatique) de la théorie des
réseaux de régulation et nous proposons une méthode de mise au point
de modèles utilisant la logique temporelle CTL.
L'exemple du système de production de mucus chez la bactérie
Pseudomonas Aeruginosa (cause principale de mortalité chez les malades
atteints de mucoviscidose) est traité. À la suite de travaux avec
Janine Guespin-Michel, microbiologiste à Rouen, nous avons prédit un
comportement pouvant potentiellement donner lieu à de nouveaux
traitements (expérience en cours au CHU de Grenoble).
========================================================================