Kevin Delmas -- PhD student ONERA / DTIM 2, avenue E. Belin 31055 Toulouse Cedex Email: email@example.com
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
2009: High 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)
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
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 Java Runtime Environmnent version 8 JRE 1.8 or newer.
- Microsoft's Z3 SMT-solver version 4.4.1 Z3 4.4.1