Les journées FAC'95 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'95 ont eu lieu les 4 et 5 avril 1995, salle de Conférence du LAAS. Programme de la journée : Mardi 4 avril 1995 9h30-11h00 Session 1 : Approches opérationnelles pour la concurrence Frédéric Boniol (DERI-CERT) Processus réactifs communicants synchrones. Pierre Azéma, Jean-Luc Albacete, François Vernadat (LAAS-CNRS) Spécification orientée classe d’un carrefour. Ahmed El Hadiri, Jean-Louis Durieux (IRIT-UPS) Les morphismes dans les réseaux de Petri. 11h00-11h30 Pause 11h30-12h30 Conférencier invité Luc Bougé (ENS Lyon) Du parallélisme de contrôle au parallélisme de données : le point de vue de la validation de programmes. 12h30-14h00 Repas 14h00-15h30 Session 2 : Vérification par preuve Jean-Paul Bahsoun, Stephan Merz, Corinne Servières (IRIT-UPS) Une logique temporelle pour les objets concurrents, et sa procédure de décision. Christel Seguin, Virginie Wiels (DERI-CERT) Un cadre logique et compositionnel pour la conception de systèmes concurrents. Pierre Bieber (DERI-CERT) Spécification et vérification avec la méthode B d’un protocole de sécurité. 15h30-16h00 Pause 16h00-17h30 Session 3 : Approches fonctionnelles pour la concurrence Camille Le Moniès de Sagazan, Bernard Berthomieu (LAAS-CNRS) Une méthodologie de typage polymorphe des calculs de processus à liaison noms-canaux dynamique. Annie Marcoux, Christine Maurel, Pascal Prieur (IRIT-UPS) La sémantique de la concurrence de PlasmaII dans le système Centaur. Christophe Coustet, Frédéric Boniol (DERI-CERT) Un apport du modèle fonctionnel à la définition de systèmes temps-réel.

La journée FAC'94 a eu lieu le vendredi 10 juin 1994, salle du 1er étage, bâtiment hexagonal du CERT-ONERA. Programme de la journée : 9h30-10h30 Conférencier invité: Ivan Lavallée, Professeur à l’Université de Paris VII Construire des algorithmes distribués à travers des schémas récursifs. 10h30-11h00 Pause 11h00-12h30 Session 1 : Méthodes Abdelmalek Benzékri, Jean-Michel Bruel, Yves Raynaud (IRIT-UPS) Développement formel d’applications réparties. Guy Durrieu, Michel Lemaître (DERI-CERT) Conception de systèmes matériels par transformation de descriptions purement fonctionnelles synchrones. Djamel Saidouni (LAAS-CNRS) Raffinement syntaxique d’actions dans LOTOS. 12h30-14h00 Repas 14h00-15h30 Session 2 : Environnement-Modèles Didier Plaindoux, Frédéric Cabestre, Nathalie Signés, Jean-Paul Bodeveix, Christian Percebois (IRIT-UPS) Objets et parallélisme: l’approche SLOOP. Martin Adelantado, Fréderic Boniol, Simon de Givry, Bernard Lécussan, R. Porche (DERI-CERT) Saturne: un modèle de description de systèmes multi-agents temps-réel et intelligents. François. Vernadat (LAAS-CNRS) Modélisation de systèmes d’agents mobiles. 15h30-16h00 Pause 16h00-17h00 Session 3 : Vérification Bruno d’Ausbourg (DERI-CERT) Modélisation et vérification en Lustre d’un protocole de contrôle d’accès à un médium de communication. Jean-Paul Bahsoun, Corinne Servières (IRIT-UPS) Formalisation des activités concurrentes - Concepts et Systèmes de Preuves.

La journée FAC'93 a eu lieu le mardi 20 avril 1993, salle de Conférence du LAAS. Programme de la journée : Les réseaux naturels. Pierre Azéma (LAAS-CNRS) Un réseau de Petri, condition-événement, construit une preuve. Il dénote donc un programme. Cette assertion est expliquée au moyen de l’illustration par des réseaux du livre de Girard, preuves et types. Il s’agit de comparer les assertions suivantes: des préconditions, une transition, des postconditions forment un réseau. Des hypothèses, une déduction, des conclusions forment une preuve. Des types, un constructeur, de nouveaux types forment un calcul. Des agents, un échange, de nouveaux agents forment un système de communication. Formalisation des objets concurrents. Jean-Paul Bahsoun, Corinne Servières (IRIT-UPS) Nous développons un système de preuve formel pour représenter et valider des concepts orientés objet dans un environnement parallèle. Deux problèmes sont étudiés : le premier concerne la composition d’un objet à partir d’autres objets plus simples , dans un environnement parallèle. Le second est celui de trouver des solutions formelles pour traiter l’interférence entre l’héritage et le parallélisme. Ces deux problèmes ont fait l’objet d’application pour les logiques non classiques comme la logique temporelle et la logique dynamique. Notre étude s’étendra vers la définition d’une nouvelle logique pour traiter ces problèmes d’une façon naturelle. Le projet LCS. Etat et perspectives. Bernard Berthomieu (LAAS-CNRS) Le langage LCS étend le langage fonctionnel Standard ML par des comportements qui permettent l’expression de programmes parallèles et communicants, et depuis lesquels peuvent être créés des processus. Le langage des comportements est basé sur une extension d’ordre supérieur du formalisme des processus communicants (CCS) de Robin Milner. Une extension non triviale du mécanisme de typage polymorphe de Standard ML permet d’inférer des types pour les comportements, le type d’un comportement associant un type polymorphe à chaque label de communication. Une technique d’exécution est définie pour les processus, conforme à la sémantique opératoire des agents CCS, et préservant les règles d’évaluation de Standard ML. PERF : un environnement de raisonnement formel. Pierre Michel, Jacques Cazin (DERI-CERT) PERF «Prototype d’Environnement de Raisonnement Formel» est basé sur le lambda-calcul typé «Logical Framework d’Edimbourg» qui permet d’encoder des logiques et de faire des vérifications de preuves par simples contrôles de types (cf. l’analogie de CurryHoward : «propositions as types»). PERF propose d’étendre le calcul LF par des facilités pour l’encodage des logiques (abréviations) et par une assistance à la construction de preuves. PERF a été utilisé dans des développements de logiciels basés sur l’approche transformationnelle, pour le passage de spécifications LOTOS à des programmes Ada, et pour vérifier des propriétés de programmes : contrôle de précision, propriétés de sécurité, propriétés des systèmes concurrents.