The real-time hybrid system widely appears in safety-critical areas including train control systems, autonomous driving systems, and so on. Safety assurance of such a system is very important. However, the behavior of such a system is complex and the environment is highly non-deterministic, which makes the safety assurance of such a system difficult to handle. We propose a periodical multi-granularity online checking and control synthesis framework to ensure the safety of a real-time hybrid system dynamically during its execution. In each cycle, we conduct online modeling and control synthesis for such systems with different granularities, online quick verification on coarse-grained models, and online accurate optimal control synthesis on fine-grained models. Part of this method had been implemented and deployed on a simulation platform of train control system successfully, that we can predict and catch the potential crash in milliseconds and stop the running train in time.
Professor, Software Institute
Nanjing University
Lei Bu is currently a professor at the Software Institute, Nanjing University. He received his bachelor's degree and Ph.D. in Computer Science from Nanjing University in 2004 and 2010 respectively. He has been visiting scholars in institutes like Carnegie Mellon University, Microsoft Research Asia, and so on. His main research interests include model checking, hybrid system, and cyber-physical system. He has published more than 50 papers in leading journals and conferences like TCAD, TC, TDSC, TPDS, TCPS, RTSS, CAV, HSCC, DATE, VMCAI, and so on. He has been awarded the NASAC Youth Software Innovation award， the Chinese computer federation young talent development program, Microsoft Research Asia Star Track young faculty program, and so on.
