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

Les journées FAC'2005 ont eu lieu les 9 et 10 mars 2005, salle de Conférence du LAAS.

Programme des journées :

Mercredi 9 mars 2005

  • 9h30 Ouverture des journées Malik Ghallab (Directeur du LAAS).

  • 9h45-10h45 Conférencier invité
    Paul Caspi (VERIMAG Grenoble)
    Approximation, échantillonnage et vote pour des systèmes mixtes continus-discrets : vers une approche unifiée.

  • 10h45-11h15 Pause

  • 11h15-12h15 Session 1 : Systèmes hybrides

    • Charles Lesire, Catherine Tessier (ONERA) Réseaux de Petri particulaires pour l’estimation symbolico-numérique.

    • Nicolas Rivière, Hamid Demmou, Robert Valette, Malika Medjoudj (LAAS) Analyse de contraintes temporelles symboliques, une approche pour la vérification de systèmes hybrides.

  • 12h15-14h00 Repas

  • 14h00-15h30 Session 2 : Conception et vérification d’architectures

    • Jean-Paul Bodeveix, Mamoun Filali, Martin Strecker (IRIT) Towards formalising AADL in Proof Assistants.

    • Christophe Kehren, Christel Seguin (ONERA) Automates AltaRica de propriétés.

    • Christophe Sibertin-Blanc, Nabil Hameurlain (IRIT, Université de Pau) Des composants intermédiaires pour la tenue de rôles dans les protocoles des systèmes multi-agents.

  • 15h30-16h00 Pause

  • 16h00-17h30 Session 3 : Vérification de modèles

    • Tarek Sadani, Jean-Pierre-Courtiat, Pierre de Saqui-Sannes (LAAS) Validating RT-LOTOS Specifications using the TINA tool.

    • Marjorie Couzinier, Louis Feraud (IRIT) Une approche formelle des diagrammes dynamiques d’UML via TLA+.

    • Florent Peres, Pierre-Olivier Ribet, François Vernadat, Bernard Berthomieu (LAAS) Vérification de propriétés invariantes par surapproximation.

Jeudi 10 mars 2004

  • 09h00-10h00 Conférencier invité
    Vlad Rusu (IRISA Rennes)
    Combiner la vérification et le test de conformité pour la validation de systèmes réactifs.

  • 10h00-10h30 Pause

  • 10h30-12h00 Session 4 : Systèmes temporels

    • Janette Cardoso, Robert Valette (IRIT, LAAS) Un nouveau graphe de classes pour la préservation des contraintes temporelles quantitatives.

    • Pierre-Olivier Ribet, François Vernadat, Bernard Berthomieu (LAAS) Vérification de systèmes temporels par sur-approximation.

    • Janette Cardoso, Sébastien Cousy, Guy Juanole (IRIT, LAAS) Extension du réseau de Petri Temporel au réseau de Petri Temporel Flou : Définition du graphe de classes d’état flou.

  • 12h00-13h30 Repas

  • 13h30-15h00 Session 5 : Modélisation

    • Philippe Balbiani, Fahima Cheickh (IRIT) Une approche uniforme de la modélisation des systèmes de protection temporisés.

    • Julien Brunel (IRIT) Logique déontique pour la spécification de la disponibilité.

    • Nil Geisweiller (ONERA) Approximation de distributions expérimentales par des termes PEPAs.