Kevin Delmas

                 Kevin Delmas -- PhD student
                 ONERA / DTIM 2, avenue E. Belin
                 31055 Toulouse Cedex




Short Biography

After an electronic and automation enducation, I obtained an engineer graduation in Automation and Electronic with a specialization in safety critical embedded systems at INSA Toulouse. I currently pursue a PhD at ONERA Toulouse focused on the application of SAT and SMT based formal method to safety assessment and safe architecture synthesis. The PhD advisors of this thesis are Claire Pagetti and Remi Delmas.



  • Now-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

  • 2009High School Diploma received at Lycee Toulouse Lautrec



  • Now--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: Cecilia, HipHOPS, GRIF

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

  • Text-Processing: Word, OpenOffice, Latex

[1]Kevin Delmas, Remi Delmas, and Claire Pagetti. Automatic architecture hardening using safety
pattern. In 34th International Conference on computer safety, reliability and security, SAFECOMP
2015, pages 283–296. Springer, September 2015.
[2]Kevin Delmas Remi Delmas and Claire Pagetti. Smt-based architecture modelling. In SIES. Springer, 2017 .
[3]Kevin Delmas Remi Delmas and Claire Pagetti. Smt-based synthesis of fault-tolerant architectures.
In International Conference on Computer Safety, Reliability, and Security. Springer, 2017.



 The KCR Analyser Tool

The KCR analyser 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 analyser 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

​More information about me