Ces journées ont été organisées par le groupe IFSE du RTRA STAE. Les journées FAC'2016 ont eu lieu les 30 et 31 mars au LAAS. Programme des journées : Mercredi 30 mars 9h00 : accueil 9h30-10h30 : Yliès Falcone, Univ. Grenoble I — LIG : On the Runtime Enforcement of (Timed) Properties. 10h30-11h00 : pause 11h00-12h30 : sûreté de fonctionnement et politiques d’informations Développement automatique d’applications tolérantes aux fautes. K. Delmas, R. Delmas, C. Pagetti Correct Instantiation of a System Reconfiguration Pattern: A Proof and Refinement-based Approach. () G. Babin, Y. Ait Ameur, M. Pantel Information exchange policies at an organisational level: formal expression and analysis. C. Saurel 12h30-14h00 : déjeuner 14h00-15h30 : sémantique et concurrence Automatic Transformation of Synchrony into Concurrency. M. Roy, P. Fraigniaud, E. Gafni, S. Rajsbaum Lightweight Specification and Analysis of Dynamic Systems with Rich Configurations. N. Macedo, J. Brunel, D. Chemouil, A. Cunha, D. Kuperberg Automates flanqués et équations de langages. S. Dal Zilio, J.-B. Raclet, F. Avellaneda 15h30-16h00 : pause 16h00-17h30 : cas d’études Latency Analysis of an Aerial Video Tracking System Using Fiacre and Tina. () S. Dal Zilio, B. Berthomieu, D. Le Botlan A Perspective on Environment Modelling for Verifying Cyber-Physical Systems. () N. Singh AADL2Fiacre. F. Zalila, E. Jenn, M. Pantel, S. Dal Zilio

Ces journées ont été organisées par le groupe IFSE du RTRA STAE. Les journées FAC'2015 ont eu lieu les 22 et 23 avril 2015 à IRIT - SITE ENSEEIHT (SALLE DES THÈSES, C002). Programme des journées : Mercredi 22 avril 9h00 : accueil 9h30-10h30 : Ahmed Bouajjani Paris 7, LIAFA : Verification of Concurrent Programs: Decidability, Complexity, Reductions. abstract: Concurrency is omnipresent in computer systems, at all levels, from applications relying on high level synchronization mechanisms and using abstract data structures, to low level code implementing concurrent/distributed data structures and system services over multi-core architectures/large-scale networks. The automated verification of concurrent programs is a challenging problem due to their highly complex behaviours. We will address the problem of verifying automatically concurrent programs, from the point of view of decidability and complexity. We will show the difficulties that raise in addressing this problem in different contexts: shared-memory, message passing, dynamic creation of tasks, recursion, relaxed memory models, etc. We will overview existing approaches for handling these issues, and we will show in particular how verification problems for concurrent programs can be reduced to ”simpler” problems (stated as reachability queries either on sequential programs, or on concurrent but sequentially consistent programs) for which there are already know verification algorithms and tools.

Ces journées ont été organisées par le groupe IFSE du RTRA STAE. Les journées FAC'2014 ont eu lieu les 16 et 17 avril 2014 à l’ONERA, salle du boulon. Programme des journées : Mercredi 16 avril 9h00 : accueil 9h15 : ouverture des journées par W. Wiels, adjointe au directeur du DTIM 9h30-10h30 : John Mullins PolyTech Montréal: Vérification et mesure du flux d’information abstract: Les politiques de sécurité du flux d'information expriment des restrictions sur l'information qui peut être acquise par les utilisateurs d'un système. Dans cet exposé, nous considérerons le problème de la vérification et de la mesure du flux d'information dans un système. La difficulté de ces problèmes réside dans le fait que, contrairement aux propriétés fonctionnelles (qualitatives ou quantitatives) des systèmes qui s'expriment comme ensembles d'exécutions, les propriétés de flux d'information s'expriment comme ensembles d'ensembles d'exécutions. Nous présenterons d'abord un schéma formel appelé opacité qui permet d'exprimer dans le cadre uniforme des systèmes de transitions, le système, l'attaquant et la politique de sécurité. Nous verrons que le problème de vérification de cette politique est décidable pour les systèmes finis, un attaquant à mémoire finie et un secret régulier. Nous verrons également comment le problème de la vérification de la plupart des propriétés de flux d'information se réduit à celui de l'opacité. Nous étendrons ensuite ce schéma au cadre des processus de décision markoviens étiquetés et poserons le problème du calcul de diverses mesures de flux d'information dans un système.

Ces journées ont été organisées par le groupe IFSE du RTRA STAE. Les journées FAC'2013 ont eu lieu les 10 et 11 avril 2013 au LAAS. Programme des journées : Mercredi 10 avril 9h00 : accueil 9h30-10h30 : Luís Soares Barbosa (HASLab - INESC TEC & Universidade do Minho, Portugal): Introducing fault propagation in a component calculus abstract: In the specification of component-based systems, relations nicely capture nondeterminism and vagueness of requirements. Probabilistic functions go a step further by quantifying the likelihood of each possible, expected or faulty, behaviour. Such a shift from qualitative to quantitative reasoning, which is becoming pervasive in Computer Science, calls for a language able to accommodate both these aspects, while preserving the polymorphic and calculational style of relational program derivation. Recently, typed linear algebra has been suggested as a suitable candidate for such a unifying rôle, when restricting to discrete probability spaces. In this talk, this framework is put at work to discuss fault propagation in a component calculus wherein components are modelled coalgebraically as (generalised) Mealy machines.

Ces journées ont été organisées par le groupe IFSE du RTRA STAE. Les journées FAC'2012 ont eu lieu les 4 et 5 avril 2012, dans l’auditorium de l’IRIT-UPS. Programme des journées : Mercredi 4 avril Accueil Café à partir de 9h00 Conférencier invité Hume: a functionally-based Domain Specific Language Targeting real-time Embedded Systems Kevin Hammond The University of St Andrews 10h30-11h00 Pause Techniques de verification 11h00-11h30 A Generic Ellipsoid Abstract Domain for Linear Time Invariant Systems P. Roux, R. Jobredeaux, P.-L. Garoche, E. Feron ONERA GEORGIA 11h30-12h00 Formal compatibility of experimental frame concept and finite and deterministic devs model D. Foures, V. Albert, A. Nkesta LAAS 12h00-12h30 Parallel Model Checking With Lazy Cycle Detection - MCLCD R. T. Saad, S. Dal Zilio, B. Berthomieu LAAS 13h00 Repas Logique et Vérification 14h30-15h00 Non preemptive static priority in network calculus: accuracy and integration with P-GPS William Mangoua Sofack, Marc Boyer ONERA 15h00-15h30 A Lemma Generator Powered by Quantifier Elimination and Hull Computation A. Champion, R.Delmas, M. Dierkes ONERA ROCKWELL 15h30-16H00 Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL A. Schimpf, S. Merz, J.-G. Smaus U. Freiburg, LORIA, IRIT 16h00-16h30 Pause Architecture 16h30-17h00 Nets-within-nets to model innovative space system architectures F. Cristini, C. Tessier ONERA 17h00-17h30 Un Point de Vue Sûreté de Fonctionnement pour la Vérification d’Architectures Abstraites M. Piriquito, P. Bieber, J. Brunel, D. Chemouil ONERA 17h30-18h00 Use of modelling methods and tools in an industrial embedded system project: works and feedback A. Fernandes Pires, S. Duprat, T. Faure, C. Besseyre, J. Beringuier, J.-F. Rolland ATOS AIRBUS

Ces journées ont été organisées par le groupe IFSE du RTRA STAE. Les journées FAC'2011 se sont déroulée les 6 et 7 avril 2011, dans la salle de conférences du LAAS. Programme des journées : Mercredi 6 avril 2011 Accueil Café à partir de 9h00 9h15 Ouverture des Journées par Jean Arlat, Directeur Adjoint du LAAS-CNRS 9h30-10h30 Conférencier invité Safraless Procedures for Timed Specifications Jean-Francois Raskin Université Libre de Bruxelles (ULB) 10h30-11h00 Pause Session 1 : Utilisation de FIACRE 11h00-11h30 Modélisation et Vérification du Double-buffer Protocole avec FIACRE Manuel Garnacho, Jean-Paul Bodeveix, Mamoun Filali IRIT 11h30-12h00 Verifying Real-Time Requirements of Timed Business Process Models Nawal Guermouche, Silvano Dal Zilio LAAS 12h00-13h30 Repas Session 2 : Preuve formelle 13h30-14h00 Premières expériences pour l’édition correcte par construction de modèles Mounira Kezadri, Marc Pantel IRIT 14h00-14h30 SMT-AI: an Abstract Interpreter as Oracle for k-induction Pierre Roux, Rémi Delmas, Pierre-Loïc Garoche ONERA 14h30-15h00 BDDs verified in a proof assistant Mathieu Giorgino, Martin Strecker IRIT 15h00-15h30 Pause Session 3 : Architectures multi-processeurs (1) 15h30-16h00 Off-line Optimal Multiprocessor Scheduling of Dependent Periodic Tasks Mikel Cordovilla, Frédéric Boniol, Eric Noulard, Claire Pagetti ONERA 16h00-16h30 Ordonnancement partitionné strictement périodique avec délais de communication sur une plate-forme IMA Ahmad Al Sheikh, Olivier Brun, Pierre-Emmanuel Hladik, Balakrishma Prabhu LAAS 16h30-17h00 Analyzing end-to-end Functional Delays on an IMA Platform Michaël Lauer, Jérôme Ermont, Claire Pagetti, Frédéric Boniol ONERA

Les journées FAC ont été organisées par le groupe SVF / FéRIA : Spécification, Vérification Formelles. Les journées FAC'2010 auront lieu les 31 mars et 1er avril 2010, salle du 1er étage du bâtiment d’accueil à l’ONERA. Préalablement aux journées FAC, José Luiz Fiadeiro a donné un cours intensif de 2 fois 3h le 30 mars sur la théorie des catégories appliquée à l’architecture des logiciels et systèmes. Programme des journées : Mercredi 31 mars 2010 9h30 Ouverture des Journées par Bernard Lecussan, Directeur du DTIM 9h45-10h45 Conférencier invité Foundations of Service-Oriented Modelling. José Luiz Fiadeiro University of Leicester 10h45-11h15 Pause Session 1 : Fondements 11h15-11h45 Calculs sur les attributs dans la réécriture de graphes fondés sur les approches catégoriques et les types inductifs. Bertrand Boisvert, Louis Féraud, Sergei Soloviev IRIT-UPS 11h45-12h15 Categorical Semantics and Non-Free Categories. Antoine El Khoury, Sergei Soloviev, Laurent Mehats, Mark Spivakovsky IRIT-UPS 12h15-14h00 Repas Session 2 : Optimisation (1) 14h00-14h30 Scheduling Analysis under Fault Bursts. Florian Many ONERA-DTIM 14h30-15h00 Collaboration entre méthode d’ordonnancement et calcul réseau. Marc Boyer, David Doose ONERA-DTIM 15h00-15h30 Pause Session 3 : Vérification (1) 15h30-16h00 Verification of the Schorr-Waite algorithm - From trees to graphs. Mathieu Giorgino, Martin Strecker, Ralph Matthes, Marc Pantel IRIT-UPS, IRIT-ENSEEIHT 16h00-16h30 Mixing induction and co-induction in Coq : a case study for lists. Celia Picard, Ralph Matthes IRIT-UPS

La journée FAC a été organisée par le groupe SVF / FéRIA : Spécification, Vérification Formelles. La journée FAC'2009 a eu lieu le 1er avril 2009, à l’auditorium de l’IRIT. Programme de la journée : Ouverture de la journée par Mamoun Filali, IRIT-UPS 9h30-10h30 Conférencier invité An informal introduction to software architecture. David Schmidt, Kansas University 10h30-11h00 Pause Session 1 : Analyse Temps Réel 11h00-11h30 Etude comparative de l’expression des protocoles de communication AADL. Lei Pi, Jean-Paul Bodeveix, Mamoun Filali IRIT-UPS 11h30-12h00 Etude du comportement temporel de données réparties. Tanguy Le Berre, Gérard Padiou, Philippe Quéinnec IRIT-INPT 12h00-12h30 Structuration des résultats de validation de systèmes temps réel par l’Ingénierie Dirigée par les Modèles : application aux études d’ordonnancement. Florian Many, David Doose ONERA-DTIM 12h30-14h00 Pause Repas Session 2 : Validation 14h00-14h30 A Multi-Periodic Synchronous Data-Flow Language. Julien Forget, Frédéric Boniol, David Lesens, Claire Pagetti ONERA-DTIM, EADS Astrium Space Transportation 14h30-15h00 Implémentation d’une technique de réduction à la volée d’espace d’états. Rodrigo Saad, Silvano Dal Zilio, Bernard Berthomieu, François Vernadat LAAS-CNRS 15h00-15h30 Pola : un langage dédié au domaine des systèmes temps réel vérifiables par model checking. Florent Peres, Pierre-Emmanuel Hladik, François Vernadat LAAS-CNRS 15h30-16h00 Pause Session 3 : Analyse statique 16h00-16h30 Analyse statique partielle pour le pire temps d’exécution. Clément Ballabriga, Hugues Cassé IRIT-UPS 16h30-17h00 Ordonnanceur vérifié pour un générateur de code automatique qualifiable. Nassima Izerrouken, Marc Pantel, Xavier Thirioux IRIT-INPT, Continental

Les journées FAC ont été organisées par le groupe SVF / FéRIA : Spécification, Vérification Formelles. Les journées FAC'2008 ont eu lieu les 3 et 4 avril 2008, salle de Conférence du LAAS. Programme des journées : Jeudi 3 avril 2008 9h30 Ouverture des Journées par Raja Chatila, Directeur du LAAS-CNRS 9h45-10h.45 Conférencier invité Contrôle des systèmes temporisés. Franck Cassez IRCCyN, Nantes 10h45-11h15 Pause Session 1 : Architectures temps-réel (1) 11h15-11h45 Programming Languages For Hard Real-Time Embedded Systems. Julien Forget, Frédéric Boniol, David Lesens, Claire Pagetti, Marc Pouzet ONERA, IRIT, EADS Astrium et LRI 11h45-12h15 Model checking prioritized time Petri nets. Bernard Berthomieu, Florent Peres, François Vernadat LAAS 12h15-14h00 Repas Session 2 : Architectures temps-réel (2) 14h00-14h30 Une approche UML pour l’analyse temporelle de communications de groupes sécurisées. Sara Mota, Thierry Villemur LAAS 14h30-15h00 -Cohérence temporelle des calculs répartis embarqués._ Nadège Pontisso, Gérard Padiou, Philippe Quéinnec IRIT 15h00-15h30 Real-Time Failure Detectors. Thomas Robert, Matthieu Roy, Jean-Charles Fabre LAAS 15h30-16h00 Pause Session 3 : Evaluation 16h00-16h30 Stochastic upper bounds for heterogeneous flows using a Static Priority Queueing on an AFDX network. Frédéric Ridouard, Jean-Luc Scharbarg, Christian Fraboul IRIT 16h30-17h00 Reliability study of a data transfer protocol with multi-redundancies packets. Guy Juanole, Tarik Khoutaif LAAS et SAGEM

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