Les journées FAC ont été organisées par le groupe SVF / FéRIA : Spécification, Vérification Formelles.

Les journées FAC'2000 ont eu lieu les 18 et 19 mai 2000 dans l’auditorium de l’IRIT.

Programme des journées :

Jeudi 18 mai 2000

  • 09h00-09h15 Ouverture des journées Luis Fariñas (directeur de l’IRIT)

  • 09h15-10h40 Session 1 : Méthodes de Vérification

    • Jean-Paul Bodeveix, Mamoun Filali (IRIT-UPS) Expérimentation de méthodes d’accélération pour la validation de systèmes paramétrés.

    • Irina Sessitskaïa (DTIM-ONERA) Vérification par abstraction des spécifications Lustre des systèmes IHM.

  • 10h40-11h00 Pause

  • 11h00-12h30 Session 2 : Vérification d’applications

    • Pierre Bieber, Jacques Cazin, Virginie Wiels, Guy Zanon, Pierre Girard, Jean-Louis Lanet (DTIM-ONERA, Gemplus) Certification d’un porte-monnaie électronique.

    • Mamoun Filali, Philippe Mauran, Gérard Padiou, Philippe Quéinnec (IRIT-UPS, IRIT-ENSEEIHT) Contrôle d’agents mobiles.

  • 12h30-14h00 Repas

  • 14h00-15h00 Conférencier invité Yves Métivier (LaBRI-IUF Talence) Algorithmique distribuée et réécritures de graphes.

  • 15h00-15h30 Pause

  • 15h30-17h00 Session 3 : Application des catégories

    • Pierre Gradit (LAAS-CNRS) L’approche catégorique des Grammaires de Graphes.

    • Marc Alter, Patrice Cros, Pierre Michel (DTIM-ONERA) Une spécification modulaire de l’architecture distribuée Corba.

Vendredi 19 mai 2000

  • 09h30-10h30 Conférencier invité Claude Kirchner (LORIA et INRIA Nancy) ELAN ou la programmation par réécriture.

  • 10h30-11h00 Pause

  • 11h00-12h30 Session 4 : Modèles de coopération

    • Janete Cardoso, Chihab Hanachi, Christophe Sibertin-Blanc (LAAS, CERISS, IRIT) Les protocoles comme composants à part entière des systèmes coopératifs.

    • José Martin Molina Espinosa, Khalil Drira, Michel Diaz (LAAS-CNRS) Modèle de description de procédures Workflow basé sur la réécriture de graphes.

  • 12h30-14h00 Repas

  • 14h00-15h30 Session 5 : Modèles temporels I

    • Gérard Bel, Fréderic Boniol, Jack Foisseau (DCSD/DTIM-ONERA) Implantation de lois de commande dans une architecture distribuée : vérification d’exigences temporelles par des méthodes de satisfaction de contraintes.

    • Brigitte Pradin-Chézalviel, Robert Valette (LAAS-CNRS) Accessibilité de marquage et logique linéaire dans un réseau de Petri t-temporel.

  • 15h30-16h00 Pause

  • 16h00-17h30 Session 6 : Modèles temporels II

    • Marc Boyer (LAAS-CNRS) Non équivalence entre les réseaux de Petri t-temporels et quelques autres modèles temporels.

    • Fréderic Boniol, Gérard Bel, Jack Foisseau (DTIM/DCSD-ONERA) Modélisation et vérification de systèmes asynchrones dans le langage synchrone Lustre : application aux systèmes avioniques.