Les journées FAC ont été organisées par le groupe SVF / FéRIA : Spécification, Vérification Formelles. Les journées FAC'2006 ont eu lieu les 23 et 24 mars 2006, auditorium de l’IRIT. Programme des journées : Jeudi 23 mars 2006 10h15 Accueil 10h30-11h30 Conférencier invité Langages Synchrones - Applications, Fondements et Evolutions. Charles André. Université de Nice-Sophia Antipolis/CNRS Session 1 : Modèles 11h30-12h00 A propos du problème de la composition des services électroniques. Philippe Balbiani, Fahima Cheikh IRIT 12h00-12h30 A state/event temporal deontic logic. Julien Brunel, Jean-Paul Bodeveix, Mamoun Filali IRIT Session 2 : Validation 14h-14h30 Recherche d’allocations sûres pour des applications avioniques. Laurent Sagaspe, Gérard Bel, Pierre Bieber, Fréderic Boniol, Charles Castel ONERA-CERT 14h30-15h00 Vérification automatique de propriétés Bossa. Jean-Paul Bodeveix, Mamoun Filali, Julia Lawall, Gilles Muller IRIT, DIKU, EMN 15h00-15h30 Pause 15h30-16h00 Vers une Méthodologie de Validation Formelle des Interfaces Homme-Machine (IHM). Alexandre Cortier, Yamine Aït-Ameur, Bruno d’Ausbourg ONERA-CERT, ENSMA 16h00-16h30 Vers une vérification d’un procédé de développement modélisé en SPEM. Benoît Combemale, Xavier Crégut, Alain Caplain, Bernard Coulette, Angel Garcia IRIT, ISYCOM, Tectosages

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.

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.

Les journées FAC ont été organisées par le groupe SVF / FéRIA : Spécification, Vérification Formelles. Les journées FAC'2003 ont eu lieu les 12 et 13 mars 2003, auditorium de l’IRIT. Programme des journées : Mercredi 12 mars 2003 9h15 Ouverture des journées Patrick Sallé (Directeur de FéRIA). 9h30-10h30 Conférencier invité Serge Haddad (Lamsade - Université Paris-Dauphine) Algèbre temporisée pour la conception, l’exécution et l’analyse de services Web. 10h30-11h00 Pause 11h00-12h30 Session 1 : Causalité Omar Tahir, Janette Cardoso, Christophe Sibertin-Blanc (IRIT-UT1) Une nouvelle approche d’intégration de diagrammes de séquence UML basée sur les RdP de haut niveau. Romulus Grigoras, Philippe Mauran, Gérard Padiou, Philippe Quéinnec (IRIT-ENSEEIHT) Ordonnancement causal de flux répartis multimédias. Jean Fanchon (LAAS-CNRS) Langages d’ordres partiels hiérarchiques: régularité et reconnaissabilité. 12h30-14h00 Repas 14h00-15h30 Session 2 : Vérification Jean Fanchon, Nicolas Rivière, Brigitte Pradin-Chézalviel, Robert Valette (LAAS-CNRS) Linear logic proofs and processes in Petri nets. Jérôme Ermont, Frédéric Boniol (DCSD/DTIM-ONERA) La vérification de systèmes temps-réel soumis à la préemption de processus est indécidable. Pierre-Olivier Ribet, François Vernadat, Bernard Berthomieu (LAAS-CNRS) Graphe de pas couvrant préservant LTL-X. 15h30-16h00 Pause 16h00-17h30 Session 3 : Systèmes embarqués Alain Fernandez, Christel Seguin, Paul Bourret (DTIM-ONERA) Optimisation du choix d’observable dans un logiciel embarqué. Christophe Kehren, Christel Seguin (DTIM-ONERA) Evaluation qualitative de systèmes physiques pour la sûreté de fonctionnement. Bernard Berthomieu, Jean-Paul Bodeveix, Jean-Marie Farines, Mamoun Filali, Pierre Michel, Pierre-Olivier Ribet, François Vernadat (SVF-FéRIA) Développement de logiciels dans les systèmes temps-réel pour l’avionique.

Les journées FAC ont été organisées par le groupe SVF / FéRIA : Spécification, Vérification Formelles. Les journées FAC'2002 ont eu lieu les 26 et 27 mars 2002, salle de Conférence du LAAS. Programme des journées : Mardi 26 mars 2002 09h45-10h00 Accueil des participants - Café 10h00-11h00 Conférencier invité François Terrier (LIST-CEA) UML, de la programmation à la modélisation : vers le développement basé sur les modèles des systèmes embarqués. 11h00-12h20 Session 1 : Méthodologie Rémi Delmas (DTIM-ONERA) Une approche méthodologique orientée composant pour la spécification des systèmes avioniques : application à Lustre. Christophe Sibertin-Blanc (IRIT - Univ. Toulouse I) Un modèle en couches pour l’ingénierie des protocoles d’interaction. 12h20-14h30 Repas 14h30-15h50 Session 2 : Etudes de cas Guillaume Lussier, Hélène Waeselynck (LAAS-CNRS) Analyse d’une preuve informelle pour guider le test. Frédéric Boniol, François Carcenac (DTIM-ONERA) Une étude de cas pour la vérification formelle de propriétés temporelles. 15h50-16h20 Pause Café 16h20-17h40 Session 3 : Temps Réel I Slim Abdelattif, Guy Juanole (LAAS-CNRS) Cadre basé sur les réseaux de Petri pour l’analyse de la qualité de service. Nathalie Chetcuti-Sperandio (IRIT-UPS) Déduction automatique à bases de tableaux en calcul des durées.

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.

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.

Les journées FAC'99 ont été organisées par le groupe de travail FAC (Formalisation des Activités Concurrentes) formé de chercheurs des trois laboratoires toulousains : IRIT-CNRS-UPS-INPT, LAAS-CNRS, DTIM-CERT-ONERA. Les journées FAC'99 ont eu lieu les 25 et 26 février 1999, salle de Conférence du LAAS. Programme des journées : Jeudi 25 février 1999 9h00-10h00 Conférencier invité Guy Juanole (LAAS-CNRS) Sur le modèle réseaux de Petri temporisés stochastiques et le concept d’automate quotient quantifié. 10h00-10h30 Pause 10h30-12h00 Session 1 : Preuve et Vérification Pierre Bieber (DTIM-ONERA) Validation modulaire d’une architecture de sécurité répartie. Jean-Paul Bodeveix, Mamoun Filali (IRIT-UPS) Preuve automatique par abstraction de problèmes à espace d’états infini ou paramétrés. 12h00-14h00 Repas 14h00-15h00 Conférencier invité Olivier Roux (IRCyN, Ecole Centrale de Nantes) Temporiser pour réduire: une contribution à la résolution du problème de l’explosion combinatoire. 15h00-17h30 Session 2 : Test et Scénarios Pascale Thévenod-Fosse, Hélène Waeselinck, (LAAS-CNRS) Test statistique d’objets concurrents réutilisables : application à une cellule de production. Marielle Doche, Christel Seguin, Virginie Wiels (DTIM-ONERA) Approche formelle du test fonctionnel de systèmes modulaires. Brigitte Pradin-Chézalviel, Robert Valette, Luis Allan Künzle (LAAS-CNRS, CEFET-PR) Formalisation de scénarios, réseaux de Petri et logique linéaire.

L’atelier AFADL'97 a été organisé par : Le groupe ADER : Développement de Spécifications et de Programmes du GDR de programmation - Pôle preuves et spécifications algébriques et le groupe FAC : Formalisation des Activités Concurrentes (Toulouse). L’atelier AFADL'97 s’est tenu les 28 et 29 mai 1997 dans l’auditorium du CERT-ONERA. Programme de la journée : Mercredi 28 mai 1997 09h15-09h45 Accueil des participants 09h45-10h00 Allocution d’ouverture de l’atelier AFADL René Jacquart (directeur du département DERI-CERT) 10h00-11h00 Conférencier invité Jean-Raymond Abrial (Consultant indépendant) Construction d’automatismes industriels avec B. 11h00-11h30 Pause 11h30-12h30 Session 1 : Conception de systèmes 11h30-12h00 Brunot Mermet, Dominique Méry (CRIN) Détection d’interactions de services : une approche avec B. 12h00-12h30 Frédéric Boniol (DERI-CERT) Discussion autour des approches synchrones pour la conception de systèmes avioniques. 12h30-14h00 Repas 14h00-15h30 Session 2 : Intégration d’approches 14h00-14h30 José-Celso Freire Junior, Jean-Pierre Giraudin (IMAG) Atelier MODSI : un outil de méta-modélisation et de multi-modélisation. 14h30-15h00 Claude Jard, Jean-Marc Jézéquel (IRISA) Vers l’utilisation d’outils de validation dans un processus de conception objet de protocoles. 15h00-15h30 Pierre Azéma, Jean-Paul Bahsoun, Pierre Michel, Virginie Wiels (LAAS, IRIT, CERT) Interaction de formalismes logiques et algébriques. Une étude de cas. 15h30-16h00 Pause 16h00-17h00 Session 3 : Processus de développement 16h00-16h30 Thomas Lambolais, Nicole Lévy, Jeanine Souquières (CRIN) Assistance au développement de spécifications de protocoles de communication. 16h30-17h00 Samira Sadaoui, Jeanine Souquières (CRIN) Quelques approches de la réutilisation dans le modèle Proplane. 17h00-18h00 Table ronde «Evolution du champ d’application des méthodes formelles.» Jean-Raymond Abrial, Didier Bert, René Jacquart, Nicole Levy, Michel Sintzoff.

Les journées FAC'96 ont été organisées par le groupe de travail FAC (Formalisation des Activités Concurrentes) formé de chercheurs des trois laboratoires toulousains : IRIT-CNRS-UPS-INPT, LAAS-CNRS, DERI-CERT-ONERA. Les journées FAC'96 ont eu lieu les 7 et 8 février 1996, auditorium de l’IRIT. Programme de la journée : Mercredi 7 février 1996 9h00-10h30 Session 1 : Systèmes temps réel critiques Laurent Lacayrelle, Abdelmalek Benzekri, Jean-Michel Bruel (IRIT-UPS) Modèles Z pour une architecture de communication temps réel. Patricia Giron (IRIT-UPS) Développement de systèmes critiques: une approche par systèmes de transitions étiquetés. Martin Adelantado, Frédéric Boniol, Augusto Burgueño, Simon de Givry, Florence Pagani (DERI-CERT) Un modèle de systèmes hybrides pour le contrôle de processus temps réel interrogeables. 10h30-11h00 Pause 11h00-12h00 Conférencier invité Dominique Mery (CRIN-Université Nancy 1) De la transformation de prédicats à la transformation de programmes. 12h00-14h00 Repas 14h00-15h00 Session 2 : Vérification I François Michel, Pierre Azéma (LAAS-CNRS) Agents permutables et algèbres de processus. François Vernadat (LAAS-CNRS) Graphes de pas couvrant. 15h00-15h30 Pause 15h30-16h30 Session 3 : Vérification II Jean-Paul Bodeveix, Mamoun Filali (IRIT-UPS) Spécification et raffinement de modèles de cohérence mémoire. Philippe Ladagnous (IRIT-UPS) Vers la vérification automatique de programmes UNITY.