La XXVI° édition des journées FAC a eu lieu les 27 et 28 mars prochain à l’IRT Saint Exupéry (bâtiment B612, Toulouse).

Ces journées sont organisées par le groupe IFSE du RTRA STAE avec un soutien spécial de l’INSA Toulouse.

Programme des journées:

Mercredi 27 mars

  • 09h00 : accueil présentation des journées et actualités du chantier IFSE par Marc Pantel

  • 09h30-10h30 : Karine Heydemann, (LIP6 / Univ. Pierre et Marie Curie): Attaques en faute: modélisation, sécurisation et analyse de robustesse de code.

    Les attaques en faute sur les systèmes embarqués sont puissantes : elles permettent de récupérer des informations sensibles, de contourner des protections, d’escalader des privilèges… S’en prémunir nécessite d’identifier les modèles de faute induits par les moyens d’injection de fautes, de concevoir des protections et de valider la robustesse de ces protections. L’exposé a pour objectif de présenter la problématique et un panorama de l’ensemble de travaux réalisés depuis plusieurs années, au LIP6 et en collaboration avec différents partenaires (académiques et industriels). Certains travaux seront présentés plus en détails. Notamment la première partie de l’exposé se concentrera sur la définition de modèle de faute à partir d’expérimentations réelles par injection d’impulsion électromagnétique. La deuxième partie de l’exposé concernera la conception de schéma de protections, notamment un mis en oeuvre à la compilation. Enfin, l’exposé se terminera par la présentation de l’outil RobustB permettant d’analyser la robustesse de code binaire soumis à des fautes. La conclusion présentera des perspectives et questions ouvertes.

  • 10h30-11h00 : pause

  • 11h00-12h30 : session chair: Philippe Queinnec

    • Petri Net Reductions for Counting Markings. Bernard Berthomieu , Didier Le Botlan, Silvano Dal Zilio

    • Identification of multi-core interference. Frédéric Boniol, Claire Pagetti and Nathanaël Sensfelder

    • Revisiting Bounded Reachability Analysis of Timed Automata Based on MILP. Iulian Ober

  • 12h30-14h00 : repas

  • 14h-15h30 : session chair: Erik Martin-Dorel

    • Experiments in Verification of Linear Model Predictive Control: Automatic Generation and Formal Verification of an Interior Point Method Algorithm. Guillaume Davy, Eric Feron, Pierre-Loic Garoche and Didier Henrion

    • Convergence and covering on graphs for wait-free robots. Armando Castañeda, Sergio Rajsbaum, Matthieu Roy

    • On the Impact of Numerical Accuracy Optimization on General Performances of Programs. Nasrine Damouche

  • 15h30-16h00 : pause

  • 16h00-17h30 : session chair: Claire Pagetti

    • Analysis and Synthesis of Weighted Marked Graph Petri Nets. Raymond R. Devillers, Thomas Hujsa

    • Event-B formalization of a variability-aware component model patterns framework. Jean-Paul Bodeveix, Arnaud Dieumegard, Mamoun Filali

    • Model Based System Engineering for Co-Simulation in Extended Enterprise. Renan Leroux, Marc Pantel, Ileana Ober, Jean-Michel Bruel

Jeudi 28 mars

  • 09h30-10h30 : Pascal Fontaine, (LORIA / INRIA & Univ. Lorraine): Quantifiers and SMT.

    Satisfiability Modulo Theories (SMT) solvers are increasingly used in verification as back-ends to check the satisfiability of formulas in presence of interpreted symbols. After a brief overview of their architecture, we will review the current methods used in those solvers to handle quantifiers. An early technique, E-matching or trigger-based instantiation, generates instances when some patterns of terms are present in the formula. Although it is experimentally quite successful, it might generate many useless instances. Model-based quantifier instantiation is a more recent semantic instantiation technique: instances are built to fix a tentative model that does not agree with the quantified formulas. An even more recent method to which we have contributed is conflict-based instantiation; it can be seen as a weaker and more efficient form of model-based instantiation, that generates only the instances that contradict the partial model in the ground solver. Finally, we will also report on our results on revisiting enumerative instantiation. These two contributions are joint work with Haniel Barbosa and Andrew Reynolds.

  • 10h30-11h00 : pause

  • 11h00-12h30 : session chair: Jan-Georg Smaus

    • Formal Verification of the Functional Layer of Robotic and Autonomous Systems. Mohammed Foughali

    • Modeling Cache Coherence to Expose Interference. Nathanael Sensfelder, Julien Brunel, et Claire Pagetti

    • Towards the qualification of an AADL model transformation tool with contracts. Christophe Garion, Jérôme Hugues et Guillaume Brau

  • 12h30-14h00 : repas

  • 14h-16h00 : session chair:

    • Reasoning about Database Queries and Updates. Mohamed Chaabani, Rachid Echahed, Martin Strecker

    • A Bounded Model Property for a Pragmatic Fragment of First-Order Linear Temporal Logic. Quentin Peyras, Julien Brunel, David Chemouil

    • Verification of Communication-Parametric BPMN Collaborations with TLA+. Sara Houhou, Souheib Baarir, Pascal Poizat, Philippe Quéinnec

    • Parabolic Set Simulation for Reachability Analysis of Linear Time Invariant Systems with Integral Quadratic Constraint. Paul Rousse, Pierre-Loic Garoche, Didier Henrion

Comité de programme

Jean-Paul Bodeveix, Mamoun Filali, Jean-Baptiste Raclet, Marc Pantel, Philippe Quéinnec, Pascal Sotin, Iulian Ober, Julien Brunel, Claire Pagetti, Pierre Roux, Silvano Dal Zilio, Pierre-Emmanuel Hladik, Didier Le Botlan, Matthieu Roy, Christophe Garion