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

Les journées FAC'2001 ont eu lieu les 25 et 26 avril 2001, salle du 1er étage, bâtiment hexagonal du CERT-ONERA.

Programme des journées :

Mercredi 25 avril 2001

  • 9h00-10h00 Conférencier invité
    Alain Finkel (ENS Cachan-LSV)
    Composition et vérification de systèmes de transitions bien structurés.

  • 10h00-10h30 Pause

  • 10h30-12h30 Session 1 : Distribution et Communication

    • Christophe Garion (DTIM-ONERA) Representation and Distribution of Requirements with a logic of Preferences.

    • Jean Fanchon (LAAS-CNRS) Automata for Partially Ordered and Partially Reliable Connections.

    • Patrice Cros et al. (DTIM-ONERA) Experience in the use of FIPA agent technologies for the development of a Personal Travel Application.

  • 12h30-14h00 Repas

  • 14h00-15h20 Session 2 : Méthodes de Validation

    • Rami El-Baida; Jean-Paul Bahsoun (IRIT-UPS) Automatic Verification of Concurrent Object Properties.

    • Charles Castel, Christel Seguin (DCSD/DTIM-ONERA) Modèles formels pour l’évaluation de la sûreté de fonctionnement des architectures logicielles d’avionique modulaire intégrée.

  • 15h20-15h50 Pause

  • 15h50-17h50 Session 3 : Applications

    • Odile Laurent, Pierre Michel, Virginie Wiels (Airbus SA - EADS, DTIM-ONERA) Using formal verification technique to reduce simulation and test effort.

    • Paul-Henry Robert, Guy Juanole (Airbus SA - EADS, LAAS-CNRS) Modélisation et évaluation d’une politique d’ordonnancement de tâches temps-réel couplée à un protocole de partage de ressources.

    • Charles Castel (DCSD-ONERA) Exemple de validation de logiciel d’UAV.

Jeudi 26 avril 2001

  • 09h00-10h00 Conférencier invité (représentant le groupe SCD-FéRIA : «Simulation Coopérative Distribuée»)
    Pierre Siron (DTIM-ONERA)
    Simulation distribuée et standard HLA : infrastructures d’exécution, applications et problèmes.

  • 10h00-10h30 Pause

  • 10h30-12h30 Session 4 : Sémantique

    • Bernard Berthomieu (LAAS-CNRS) Analyse de réseaux de Petri temporels. La méthode des classes d’états et sa mise en oeuvre.

    • Janete Cardoso, Christophe Sibertin-Blanc, Chantal Soulé-Dupuy (IRIT - Université Toulouse 1) Une sémantique formelle des diagrammes d’interaction d’UML via les réseaux de Petri.

    • Pierre Gradit, François Vernadat (LAAS-CNRS) Comportement d’un système de réécriture.