>> Title: Verification of Hybrid Systems by Structural Analysis
>>
>>
>> Abstract:
>>
>> In this talk, we present two approaches for structurally analyzing
>> the behavior of nonlinear hybrid systems which are dynamical systems
>> equipped with both continuous flow and discrete jumps.
>>
>> In the first approach, we decompose a continuous dynamics by relaxing
>> the dependencies among the state variables, and then perform the
>> reachability computation for the decomposed model in a hybridization
>> framework in order to ensure the conservativeness. Our experiment
>> shows that the decomposed method greatly improves the scalability of
>> the existing reachability algorithms.
>>
>> The second approach shows a compositional way to compute a relational
>> abstraction for a hybrid system.
>> A relational abstraction is a finite state discrete system which
>> captures all behavior of a hybrid system at discrete time steps in a
>> bounded region.
>> The main advantage of using relational abstractions is that we may
>> treat the system components individually and compose them in the end
>> by just specifying their dependencies using constraints. Then the
>> properties on a hybrid system can be verified by applying software
>> model checkers to its abstraction model.
>>
>> Both of the approaches demonstrate that structural analysis has a lot
>> of potential to formally verify properties for large-scale systems.
>>
>>
>>
>> Short Bio:
>>
>> Xin Chen is an assistant professor in the Department of Computer
>> Science at the University of Dayton.
>> He received a degree of doctor of natural sciences (Dr. rer. nat.)
>> from RWTH Aachen University in 2015 and was a postdoctoral researcher
>> at the University of Colorado Boulder from 2015 to 2018.
>> His main research interests include formal methods, safety and
>> security of Cyber-Physical Systems (CPS), numerical and interval
>> analysis, real-time systems, and the theory of differential equations.
>> He has been involved in several projects funded by NSF, Toyota and
>> AFRL to develop techniques to analyze medical devices, self-driving
>> cars and aircraft systems. Besides, he is the primary developer of
>> Flow* which is a verification tool for nonlinear CPS.