1. Home
  2. Kevin Delmas

Kevin Delmas

Biography and Research interests

Kevin Delmas -- Reasearch engineer  ONERA/DTIS
2, avenue E. Belin
31055 Toulouse Cedex
Tel:(+33)5-62-25-28-49
Email: kevin.delmas@onera.fr
ORCID: ORCID iD icon0000-0002-7654-0332

Short Biography

After an electronic and automation education, I obtained an engineer graduation in Automation and Electronic with a specialization in safety critical embedded systems at INSA Toulouse. I pursued a PhD at ONERA Toulouse focused on the application of SAT and SMT to safety assessment and safe architecture synthesis with Claire Pagetti and Remi Delmas. Since then, I am working as a research engineer at the ONERA Toulouse lab, my main research topics are:

  • the use of formal methods to assist design and certification of embedded systems
  • safety assessment methodologies for autonomous systems
  • the development of model-based safety assessment methods and tools
  • safety-driven architecture optimization relying on IA based methods

 

Research

Safety assessment and certification of embedded and autonomous systems 

Students

Current PhDs

  Former post-docs

Education

  • 2017-2014: PhD thesis at ONERA Toulouse  on the development environments  and methods for synthesis of predictable and fault tolerant systems .   Short abstract: Safety is one of the main guidelines for system design. Designers are in charge to develop architectures that comply with the safety requirements. We propose an automatic hardening method based on the exploration of possible designs to build safe systems. The method uses the state-of-the-art safety analysis methods and SMT solver to propose an efficient resolution of safety driven exploration problem.

  • 2014--2009:  Engineer graduation in automation, electronic and safety critical embedded systems at INSA Toulouse

  • 2009: High School Diploma received at Lycee Toulouse Lautrec

 

Experience 

  • Now - January 2018: Research engineer at ONERA Toulouse, main research topics are:
    • the development of model-based safety assessment methods and tools
    • the use of formal methods to perform safety assess
    • safety-driven architecture optimization relying on IA based methods
    • new safety assessment methodologies for autonomous systems
  • December 2017--November 2014: PhD thesis at ONERA Toulouse on the development environments  and methods for synthesis of predictable and fault tolerant systems .

  • February 2014: Master Internship at ONERA Toulouse on the conception of fault tolerant multi periodic longitudinal controller on many core target:

  • ​Survey of classical fault tolerance techniques

  • Suggestion of development cycle for controller conception

  • Formalization of automatic hardening techniques and implementation of a demonstrator on Matlab with Cecilia OCAS interface

  • Application of hardening on longitudinal controller and simulation with SchedMCore tool

  • June 2013: ​Bachelor Internship at MyFox Labege, conception of communication card for ZigBee Home Automation wireless protocol:

  • ​Auto training on ZigBee Home Automation standard

  • Hardware and software solution designer (TI CC2530)

Computer skills

  • System Modelling: AADL, Matlab, Simulink, UML

  • Safety Modelling: Altarica, HipHOPS, GRIF

  • Program Languages: C, Java, Scala, Android, SCADE, Lustre , Prelude

  • Text-Processing: Word, OpenOffice, Latex

Publications
Developments and Tools

The PML Analyzer

The PML analyzer is an open source API providing a simple DSL to build
a description of the architecture of your chip based on the PHYLOG Model Language (PML).
From this representation a set of safety and interference model templates can be generated to perfom safety and
interference analyses of your platform.

The KCR Analyzer Tool

The KCR analyzer is a model-based safety analysis tool for static systems described in the KCR language. This tool is a an implementation of the methods developped in my PhD on "Automatic Synthesis of Fault tolerant Architectures " tutored by Claire Pagetti and Remi Delmas. The manuscript is available here and the presentation slides are available here.

The KCR analyzer provides the following safety analyses using SMT-based and BDD-based techniques.

  • computation of reliability
  • computation of minimal cutsets (called MCS)
  • computation of minimal cardinality of MCS (without computing them)
  • check cardinality requirement on MCS (without computing it)
  • check system monotony
  • check reliability requirement
  • solve exploration problem

And the following extra features are provided 

  • dot export of the Binary Decision Diagram of the structure function
  • package management
  • syntax highlighting for emacs
The analyser, benchmark systems and installation guide are available here. 
The source code and documentation are available here
Demonstration videos of system analysis and design space exploration problem solving are available respectively here and here.
The only dependencies of the KCR analyzer are:
  • The Java Runtime Environmnent version 8 JRE 1.8 or newer.
  • Microsoft's Z3 SMT-solver version 4.4.1 Z3 4.4.1
Teaching

  • Safety assessment of critical systems

    • Introduction to safety assessment of static and dynamic systems at ISAE SEN and EMS masters, ENSEEIHT, INSA Toulouse and Ecole Centrale Nantes
    • Safety assessment of autonomous systems at ISAE

  • Functional programming

    • Introduction to functional programming language Scala 3.0 at ISAE 

  • Constraint programming

    • Introduction to SAT and SMT solver at ENSEEIHT