I was involved into the following research directions:
and particularly into the following themes:
- Fault tolerant real time system, while I worked on embedded Jet Engine Control we developed a reconfigurable computer able to guarantee hard deadline even in presence of hardware fault and dynamic reconfiguration. For that purpose we implemented a real time scheduler with Earliest Deadline first policy plus heuristics for the load balancing problem while reconfiguration occurred. This was the subject of my thesis and some publications. I've worked also into emebedded Neural Network into a virtual machine to detect run time faults.
- Fault prevention, using formal methods we evaluated some technologies for the smart card domain (Abstract interpretation, thermo proving, model checking), and used the B Method to develop a prototype (part of the Matisse project). This has been the subject of L. Casset thesis. Following this work we decided to design our own formal tool; based on the WP-calculus and the JML language in order to help Gemplus developers to develop in a safe way their Java programs. Our tool has been transferred at the INRIA research institute. I work with Razika on formal proof of Java Card update mechanism.
- Fault elimination, this objective of this work was to propose a methodology and associated tool to generate automatically test suites from either UML model or JML specification (part of the RNTL Cote project). This was the subject of H. Martin thesis. Recently I'm working on model based testing with Aymerick Savaray PhD student.
- Security evaluation, in the specific case of open smart card with sharing capacities we need to tackle the information flow problem (see PACAP project). We used abstract interpretation and model checking techniques. More recently we investigate the security of the firewall mechanism in Java Card. I have a PhD student working on fault impact evaluation throught SFI simulation. My student Samyia is developping a tool to evaluate the possibility to hide agressive code into a well formed code.
- Secure embedded system, after a technological transfer from the university of Lille (the Camille prototype) we developed some tools to adapt it to the Java Card model, and developed our own on-the-fly compiler. The underlying technologies were : exo-kernel and embedded compiler. We are currently investigating the security of embedded web server in tiny devices and on-line fault detection.