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.

  • 10h30-11h00 : pause

  • 11h00-12h30 : techniques de vérification

    • Computing Quadratic Invariants with Min- and Max-Policy Iterations: a Practical Comparison P. Roux and P.-L. Garoche

    • Classes d’états réduites par symétrie pour les réseaux de Petri temporels P.-A. Bourdil, B. Berthomieu, F. Vernadat

    • Towards a certified Petri net model-checker L. Fronc and F. Pommereau

  • 12h30-14h00 : déjeuner

  • 14h00-15h30 : logique

    • A Logic with Revocable and Refinable Strategies C. Chareton, J. Brunel and D. Chemouil

    • Logical Foundations for Reasoning about Transformations of Knowledge Bases M. Chaabani, R. Echahed and M. Strecker

    • Binding Structures as an Abstract Data Type W. Ricciotti

  • 15h30-16h00 : pause

  • 16h00-17h00 : analyse de sûreté de fonctionnement

    • Specifying Safety Monitors for Autonomous Systems using Model-checking M. Machin, F. Dufossé, J.-P. Blanquart, J. Guiochet, D. Powell, M. Roy and H. Waeselynck

    • Probabilistic Failure Analysis in Model V&V N. Ge, M. Pantel and X. Crégut

Jeudi 17 avril

  • 9h30-10h30 : Nicolas Markey LSV, ENS Cachan: Temporal logics for multi-agent systems

    abstract:

Temporal logics are a convenient formalism for reasoning about computer systems. When the global systems includes several components having different roles, classical temporal logics (CTL, LTL) are not sufficient. Alternating-time Temporal Logic (ATL) was proposed as a solution for this. In this talk, I will explain why ATL is not sufficient, as it can only express antagonistic objectives. I will then present a modified semantics for ATL, which can express mixed antagonistic and collaborative objectives. This semantics makes the logic much more expressive, but we will see that it also makes the verification problems much more complex. This talk is based on joint works with Thomas Brihaye, Arnaud Da Costa and François Laroussinie.

  • 10h30-11h00 : pause

  • 11h00-12h30 : modélisation et véfication formelles

    • Contrats de sûreté pour composants réactifs temporisés en SysML I. Dragomir, I. Ober and C. Percebois

    • Étude de cas du train d’atterrissage; un cas d’étude pour Fiacre B. Berthomieu, L. Fronc and S. Dal Zilio

    • Adding Contextual Guidance to the Automated Search for Probabilistic Test Profiles S. Poulding and H. Waeselynck

  • 12h30-14h00 : déjeuner

  • 14h00-15h30 : techniques de vérification

    • Policy iterations in finite templates domain A. Adjé

    • Implementation of two Algorithms for the Threshold Synthesis Problem C. Schilling, J.-G. Smaus and F. Wenzelmann

    • Verification of redecoration for infinite triangular matrices in Coq C. Picard and R. Matthes

  • 15h30-16h00 : pause

  • 16h00-17h00 : temps réel

    • Run-time Control to Increase Task Parallelism in Mixed-Critical Systems A. Kritikakou, O. Baldellon, C. Pagetti, C. Rochange, M. Roy

    • The ROSACE Case Study: From Simulink Specification to Multi/Many-Core Execution C. Pagetti, D. Saussié, R. Gratia, E. Noulard and P. Siron