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

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

Programme des journées :

Jeudi 15 mars 2007

  • 9h15 Accueil

  • 9h30-10h.30 Conférencier invité
    Conceptions Formelles - L’utilisation de vérificateurs de modèles pour débugger des cahiers des charges et proposer des solutions architecturales valides.
    Alain Griffault LABRI et Université de Bordeaux

  • 10h30-11h00 Pause

  • Session 1 : Architectures - AADL

    • 11h00-11h30 Assessment of the AADL Behavioral Annex. Ricardo Bedin França, Jean-François Rolland, Mamoun Filali Amine, Jean-Paul Bodeveix, David Chemouil IRIT et CNES

    • 11h30-12h00 Aide à la conception multi points de vue de systèmes embarqués. François Revest, Frédéric Boniol, Claire Pagetti ONERA-DTIM et IRIT

    • 12h00-12h30 AADL Modeling of a Generic Bus. Ricardo Bedin França, Mamoun Filali Amine, Jean-Paul Bodeveix IRIT

  • 12h30-14h00 Repas

  • Session 2 : Validation et Vérification (1)

    • 14h00-14h30 Vérification formelle d’exigences temporelles avec génération automatique d’observateurs. Benjamin Fontan, Pierre de Saqui-Sannes, Ludovic Apvrille LAAS-CNRS

    • 14h30-15h00 Rétro-Ingénierie et Validation Formelle des Systèmes Interactifs : Application au Langage Java/Swing. Alexandre Cortier, Yamine Aït-Ameur, Bruno d’Ausbourg ONERA-DTIM, LISI/ENSMA

    • 15h00-15h30 Mobile Systems from a Validation Perspective: a Case Study. Hélène Waeselynck, Zoltan Micskei, Minh Duc NGuyen, Nicolas Rivière LAAS-CNRS

  • 15h30-16h00 Pause

  • Session 3 : Validation et Vérification (2)

    • 16h00-16h30 SimplePDL2Tina : Mise en oeuvre d�une Validation de Modèles de Processus. Benoît Combemale, Xavier Crégut, Bernard Berthomieu, François Vernadat IRIT, LAAS-CNRS

    • 16h30-17h00 Génération de séquences de test temporisées à partir de réseaux de Petri temporels à chronomètres. Noureddine Adjir, Pierre de Saqui-Sannes, Kamel Rahmouni LAAS-CNRS

Vendredi 16 mars 2007

  • 9h00-10h00 Conférencier invité
    Une extension conservative du data-flow synchrone avec des machines à état.
    Marc Pouzet LRI, Université Paris-Sud 11 et INRIA

  • 10h00-10h30 Pause

  • Session 4 : Cadres de Modélisation et de Vérification

    • 10h30-11h00 Spécification et Vérification par Interprétation Abstraite d’Aspects pour la Distribution. Pierre-Loïc Garoche, Marc Pantel, Xavier Thirioux IRIT

    • 11h00-11h30 Chronogrammes et contraintes pour la modélisation à de systèmes dynamiques à évènements discrets. Gérard Verfaillie, Cédric Pralet, Michel Lemaître ONERA-DCSD

    • 11h30-12h00 Modeling and Verifying Graph Transformations in Proof Assistants. Martin Strecker IRIT

  • 12h00 Fin des journées