
LRI (Université ParisSud 11) ,
CentraleSupélec Lina YE
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 realtime or hybrid systems (cyberphysical systems) due to continuous evolutions. Recently, my major research work has focused on the analysis of realtime 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.
Publication resume: one book chapter, 3 journals and 27 international conferences, among which 15 conferences are ranked by A*, A or B (CORE Ranking)
