(Université Paris-Sud 11) ,
PhD, Associate Professor
|Address||3 rue Joliot-Curie, 91192 Gif-sur-Yvette
|Bât 650 Ada Lovelace, Université Paris Sud |
| 91405 Orsay
- Formal methods
- Model-based diagnosis (diagnosability, predictability, manifestability) and model-based testing
- Formal verification of complex systems (concurrent and distributed discrete event systems, real-time and hybrid systems, probabilistic and controlled systems)
- Analysis of cyber-physical systems (Counterexample-guided Abstraction Refinement (CEGAR), SMT, and reinforcement learning)
- CSP refinement proof with Isabelle/HOL
The main axes of my research focus on the analysis of complex systems on the design stage by using formal methods. I am particularly interested in the formal verification of important diagnosis related properties, such as diagnosability, predictability, manifestability, as well as safety and security.
Diagnosability is an important property that determines at the design stage whether a diagnosis algorithm can be designed on a partially observable system, i.e., whether one can determine with certainty the occurrence of the fault after some delay. Predictability describes the system's ability to predict with certainty the future occurrence of a fault when it still in a normal state. One important application of this could be the prediction of malicious actions on cloud systems to avoid them. Inspired by the philosophy that if two systems are mentally different, then there must be some contexts in which this difference will display itself in differential physical consequences, we have proposed manifestability. Manifestability is a property that determines the capability of a system to manifest a fault occurrence in at least one future behavior, which is thus considered as the weakest requirement on observations for having a chance to identify on line fault occurrences.
For complex systems, one major challenge for formal analysis is how to deal with the combinatorial explosion of the search space, which is sometimes even infinite, such as real-time or hybrid systems (cyber-physical systems) due to continuous evolutions. Recently, my major research work has focused on the analysis of real-time systems modeled as timed automata using SMT, and that of hybrid systems modeled as hybrid automata using CEGAR. Now I am especially interested in the analysis of probabilistic models because uncertainty is actually an intrinsic nature of many real systems, which can be captured by probability theory. On the other hand, i'd like to also take advantage of mature techniques of reinforcement learning to prove or falsify safety properties of infinite state models.
I studied computer science and system information in University of Surrey, England and University of Paris-Sud 11. Then I received the PhD degree in Computer Science from University of Paris-Sud 11, France, in 2011. I held a post-doctoral position in the research team CONVECS at Inria Rhône-Alpes in 2012-2014. I am currently an associate professor of computing science at CentraleSupélec and carry out my research work at the LRI laboratory (University of Paris-Sud 11), France.
- Reviewer for journals: IEEE Transactions on Automatic Control, IEEE Access, Journal of Systems and Software, Science of Computer Programming
- PC member: FOCLASA'17, FOCLASA'18, FOCLASA'19, Digicosme Spring School ForMaL 2019, VALID'15, VALID'16
- Reviewer for conferences: ACC'18, COMPSAC'17, CDC'16, FACS'16, ACC'16,
Publication resume: one book chapter, 3 journals and 27 international conferences, among which 15 conferences are ranked by A*, A or B (CORE Ranking)
- Lulu He (from february 2019)
- Hadi Zaatiti (co-supervisor: Philippe Dague, Jean-Pierre Gallois)
- Hassan Ibrahim (co-supervisor: Philippe Dague, Laurent Simon)