Allez au contenu, Allez à la navigation

.

RSS

Rémi Delmas

Research Interests

I joined ONERA in 2009. My research focuses on the integration of SAT, MaxSAT and SMT solvers at various levels of the development process for critical embedded systems:

  • At the architectural level: 
    • Safety assessment and fault-tolerant design  using model based techniques:
    • Verification oapplication mapping safety (IMA modules) and communication mapping safety (AFDX networks).
    • IMA application deployment synthesis and optimization under safety, functional and real-time constraints using SAT and MaxSat solvers.
  • At the software level :
    • critical synchronous software modelling and verification using SAT and SMT-based techniques.

I sometimes venture out of embedded systems (see project deontic information diffusion policies below).

I have been or am currently involved in the following projects (in inverse chronological order):

  • 2012-2016: CAFEIN ANR project: IC3/PDR formal verification algorithms for synchronous programs (Lustre, Scade)
  •  2011-2015: PR MAPEIS (internal project): creating a formal specification language and associated SMT-based model-cheker dedicated to the expression and verification of information sharing policies, in the context of European space situation awareness (a system of systems).
  • 2011-2014: PR SCC (internal project): Allocating tasks to cores and communication links in the Network On Chip in the Intel 48-cores SCC processor, while minimizing network congestion and communication latency, using MaxSAT techniques.
  •  2010-2012 OGRE project (Airbus): Automatically routing and optimizing the wiring of aircraft sensors under safety constraints, while minmizing the weight of the wiring.
  • 2009-present PAM (DGAC+Airbus), PR MAUSART (interal) projects : Supporting the design space exploration of Integrated Modular Avionics applications and platforms under safety and real-time constraints, using SAT and MaxSAT techniques.
  • 2009-present PAM (DGAC+Airbus), PR MAUSART (internal) projects: Automatically allocating tasks to IMA computing modules while optimizing the routing of VirtualLinks in the AFDX network, under safety constraints, using MaxSAT techniques.
  • 2009 - 2011 : MISSA FP-7 project (European Union): Allocating DAL levels and failure probability budgets to aircraft functions, and selectively downgrading DAL levels in coherence with ARP-4754 guidelines, by taking into account the way in which the failure modes are combined in a given set of Failure Conditions, using MaxSAT and linear programming techniques.

Phd Students

  • 2014-2017: with Claire Pagetti, advising PhD student Kevin Delmas, on the topic of evaluating multi- and many-core processors for safety critical real-time embedded applications and designing a suitable development chain, taking into account safety, functional and real-time requirements from high-level application design to code generation for the multi/many-core target to verification/validation (of course, SAT and/or SMT solvers will be used at some point in this thesis).
  •  2011-2014: advising Adrien Champion, on the topic of proving properties of synchronous dataflow programs by combining various SMT-based techniques such as k-induction, quantifier elimination, numerical lemma generation using polyhedral computations, property directed reachability analysis, etc.

Papers

You can find some of my papers on DBLP.

Tools

I contribute the development of, or am the main author of the following software tools :

  • TUFF: an smt-based parallel model checker for synchronous transition systems, including k-induction, quantifier elimination and numerical lemma generation heuristics;
  • SMT-QE: a tool for efficient SMT-based quantifier elimination for quantifier free first order formulas mixing boolean, linear real and integer arithmetic theories;
  • DALculator: a MaxSAT-based tool for automatic independence requirements generation,  automatic allocation of Development Assurance Levels (DALs) and allocation of failure probability budgets to IMA functions, based on minimal cut sets information;
  • Peps & Peps-analyzer: a formal language an associated SMT-based property prover for deontic information sharing policies;
  • eLogical: A grounder for many-sorted first order logic formulas interpreted over finite domains to pure SAT, used for various tasks inside ONERA (task mapping, communication routing, scheduling, etc.).

(Links to be added soon).