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.

  • 10h30-11h00 : pause

  • 11h00-12h30 : systèmes temps-réel

    • Mapping a Multi-Rate Synchronous Language to a Many-Core Processor Wolfgang Puffitsch, Eric Noulard, Claire Pagetti

    • On existence of global trajectories of non-deterministic systems Ievgen Ivanov

    • A Component-Based Framework for Modeling and Analyzing Probabilistic Real-Time Systems L. Santinelli, P. Meumeu Yomsi, D. Maxim and L. Cucu-Grosjean

  • 12h30-14h00 : déjeuner

  • 14h00-15h30 : vérification dynamique

    • Detection of interferences in aspect-oriented programs using executable assertions Jimmy Lauret, Helene Waeselynck, Jean-Charles Fabre

    • Efficient Online Analysis of Accidental Fault Localization for Dynamic Systems using Hidden Markov Model Ning Ge, Nakajima Shin (NII, Japon) et Marc Pantel

    • Distributed Monitoring of Temporal System Properties using Petri Nets Olivier Baldellon, Matthieu Roy, Jean-Charles Fabre

  • 15h30-16h00 : pause

  • 16h00-17h00 : logique

    • Updatable strategy logic Christophe Chareton, Julien Brunel, David Chemouil

    • À propos d’une logique dynamique pour la réécriture de termgraphs Mathias Winckel

Jeudi 11 avril

  • 9h30-10h30 : Stephan Merz (Loria) : Lessons Learnt During The Verification of Distributed Consensus Algorithms
abstract:

Distributed algorithms are often quite subtle, in the way they operate and in the assumptions they make. Formal verification is therefore crucial in distributed computing. Consensus is the paradigmatic problem for algorithms that must tolerate faults, and it is well known that Consensus is impossible to implement in asynchronous settings. Many algorithms exist, but they are hard to compare because they are presented in different computational models and with different assumptions about message synchrony and failure hypotheses, and they are rarely proved correct.

We have formally verified different Consensus algorithms tolerating various kinds of failures (including benign and Byzantine failures). All algorithms were expressed in the Heard-Of model, a uniform computational model that allows us to compare the assumptions under which the algorithms operate. Our proofs are made possible by the observation that (almost) all known Consensus algorithms are structured in communication-closed rounds. Formally, we prove a reduction theorem that can be retraced to Lipton’s seminal paper (1975) or Zwiers’ work communication-closed layers in the early 1990s, and that allows us to pretend that nodes operate in lock-step.

In this talk, we will present the main ideas underlying our development, and particularly insist on the importance of choosing appropriate high-level abstractions.

(Joint work with Bernadette Charron-Bost, CNRS & LIX, and Henri Debrat, Univ. de Lorraine & LORIA)

  • 10h30-11h00 : pause

  • 11h00-12h30 : méthodes formelles (1)

    • Mechanized Semantics of Real-Time Concurrent Systems Manuel Garnacho, Jean-Paul Bodeveix, Mamoun Filali

    • Model-based formal specification of a DSL library for a qualified code generator Andres Toom, Arnaud Dieumegard, Marc Pantel

    • Towards Certifying Network Calculus Etienne Mabille, Marc Boyer, Loïc Fejoz, Stephan Merz

  • 12h30-14h00 : déjeuner

  • 14h00-15h30 : méthodes formelles (2)

    • Formal Verification of a Safety Argumentation and Application to a Complex UAV System Julien Brunel, Jacques Cazin

    • Formal Software Verification at Model and at Source Code Levels Anthony Fernandes Pires, Thomas Polacsek and Stéphane Duprat

    • A Formal Model of Resource Sharing Conflicts in Multithreaded Java Nadezhda Baklanova, Martin Strecker

  • 15h30-16h00 : pause

  • 16h00-17h00 : techniques de vérification

    • Coarse-Grained Locking Scheme for Parallel State Space Construction Rodrigo T. Saad, Silvano Dal Zilio and Bernard Berthomieu

    • Integrating Policy Iterations in Abstract Interpreters Pierre Roux et Pierre-Loïc Garoche