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

Les journées FAC'2004 ont eu lieu les 9 et 10 mars 2004, salle du 1er étage, bâtiment hexagonal du CERT-ONERA.

Programme des journées :

Mardi 9 mars 2004

  • 9h30 Ouverture des journées Jacques Cazin (Directeur du DTIM).

  • 9h45-10h45 Conférencier invité
    Jean-Pierre Elloy (IRCCyN-Nantes)
    Présentation de la démarche de conception des architectures logicielles embarquées dans l’automobile: de la définition des exigences à l’implantation des tâches exécutables. Le rôle et les démarches de modélisation et de validation dans ce schéma.

  • 10h45-11h15 Pause

  • 11h15-12h15 Session 1 : Scénarios

    • Malika Medjoudj, Sarhane Khalfaoui1, Hamid Demmou, Robert Valette (LAAS-CNRS, PSA Peugeot Citroën) Un algorithme pour l’extraction des scénarios critiques dans les systèmes hybrides.

    • Jean Fanchon (LAAS-CNRS) Regular sets of pomsets without autoconcurrency : Extending regular MSC languages.

  • 12h15-14h00 Repas

  • 14h00-15h30 Session 2 : Spécification

    • Jean-Paul Bodeveix, Mamoun Filali, Miloud Rached (IRIT-UPS) Méthodes de spécification de systèmes temps réel en B.

    • Pierre Bieber, Charles Castel, Christophe Kehren, Christel Seguin (DTIM&DCSD-ONERA) Safety Architecture Patterns : une introduction.

    • Christophe Mareschal de Charentenay (SupAéro-ONERA) Adaptation d’un langage de description d’architecture à l’expression du comportement. Application.

  • 15h30-16h00 Pause

  • 16h00-17h30 Session 3 : Distribution - Coopération

    • Vincent Hennebert, Marc Pantel (IRIT-ENSEEIHT) Typage de comportements non uniformes. Application à JavAct.

    • Aurélie Hurault, Marc Pantel (IRIT-ENSEEIHT) Introduction de la répartition et da la mobilité dans le calcul concurrent CAP : Étude bibliographique.

    • Karim Guennoun, Khalil Drira, Michel Diaz (LAAS-CNRS) Architectures logicielles distribuées dynamiques, caractérisation de quatre styles de base.

Mercredi 10 mars 2004

  • 09h00-10h00 Conférencier invité
    Patricia Bouyer (LSV-ENS-Cachan)
    Les automates temporisés, de la théorie à la pratique.

  • 10h00-10h30 Pause

  • 10h30-12h00 Session 4 : Modèles temporisés

    • Jean-Paul Bodeveix, Mamoun Filali, Odile Nasr (IRIT-UPS) Spécification d’ordonnanceurs temps réel.

    • Pierre de Saqui-Sannes, Ludovic Apvrille, Christophe Lohr, Jean-Pierre Courtiat (LAAS-CNRS, ENSICA, ENST, Université Concordia de Montréal) Derniers développements autour du profil UML temps réel TURTLE.

    • François Carcenac, Frédéric Boniol, Zoubir Mammeri (DTIM-ONERA, IRIT-UPS) Définition d’un modèle formel pour la spécification et la vérification de la Qualité de Service temporelle.

  • 12h00-13h30 Repas

  • 13h30-15h00 Session 5 : Vérification et test

    • Marc Boyer, Jean-Christophe Pince (IRIT-ENSEEIHT, M3-Systems) Model-Checking aléatoire: une approche entre test et vérification.

    • Bruno d’Ausbourg, Nil Geisweiller (DTIM-ONERA) La modélisation de simulations distribuées pour l’évaluation de performance par les techniques formelles probabilistes.

    • Guillaume Lussier, Hélène Waeselynck (LAAS-CNRS) Test Guidé par la Preuve. Etude expérimentale sur l’algorithme d’appartenance de groupe du TTP/C.