9h30
Accueil des participants
10h00
Conférence Invitée : Utilisation des outils synchrones et des outils d'interprétation abstraite en contexte industriel
Daniel Pilaud
10h45
Pause
11h15
Interprétation de spécifications temporelles à l'aide d'un outil de preuve
Dominique CANSELLet Dominique MERY
11h55
Une notion effective d'équivalence pour des familles de scénarios représentées par des HMSCs
Loic HELOUET Claude JARD et Benoit CAILLAUD
12h35
Déjeuner
14h00
Description d'architecture logicielle par connexion de machines abstraites
Yves LEDRU et Remy SANLAVILLE
14h40
Schema générique de développement par composition
L. CORRENSON, E. DURIS, D. PARIGOT et G. ROUSSEL
15h20
Le raffinement vu comme primitive de spécification - une comparaison de VDM, B et Specware
Yves LEDRU, Catherine ORIAT et Marie-Laure POTET
16h00
Pause
16h30
Using the B Method for Modelling Protocols
Jean Louis LANET
17h10
Table Ronde. Discussion
Preuves et tests dans le processus de développement de logiciels
JR. Abrial, P. Ayrault (Cervantec), A. Faivre (Matra Transport), R. Groz (CNET/France Télécom), C. Jard (CNRS/IRISA), JN. Monfort (Aerospatiale), D. Pilaud (INRIA)
18h10
Réception et diner.
9h00
Conférence Invitée : Les méthodes formelles et le génie logiciel chez France-Télécom
Roland Groz
9h45
Pause
10h15
Simulation of Distributed RPC based Communications
Thierry CATTEL et Gregory DUVAL
10h55
Développement d'une spécification formelle en UNITY. Analyse d'un système de contrôle d'accès
Mamoun FILALI, Gerard PADIOU et Philippe QUEINNEC
11h35
Présentation d'un banc d'essai pour l'évaluation des méthodes formelles basé sur l'étude de cas du contrôle d'accès - Appel à contributions
Yves LEDRU, Gerard PADIOU, Jacques JARAY
12h15
Déjeuner
14h00
Extension des spécifications B par de la logique temporelle linéaire pour décrire des propriétés dynamiques de systèmes réactifs
Jacques JULLIAND et Francoise BELLEGARDE
14h40
Analyse Temporelle de Systemes Temps Réel à l'Aide de Réseaux de Petri : PeNSMARTS
Emmanuel GROLLEAU, Annie CHOQUET-GENIET, Francis COTTET
15h20
Pause
Session 6 : Développements de Spécifications II
15h50
Construction et réutilisation de spécifications LOTOS
Samira SADAOUI
16h30
Modélisation sous RHODES d'un procédé de développement formel. Application à la spécification en Unity .
Xavier CREGUT et Bernard COULETTE
17h10
Perspectives et Cloture de l'Atelier AFADL