Chennai Mathematical Institute


12:00 noon, Seminar Hall
Scalable Dynamic Analysis of Large Linear Hybrid Systems

Parasara Sridhar Duggirala
University of Connecticut, USA.


Safety critical Cyber-Physical Systems (CPS) such as air-traffic control systems, autonomous vehicles, medical devices, etc. should always satisfy their respective safety specification. Violation of such safety specification can lead to loss of property or life. One of the widely used technique for ensuring that a CPS satisfies it safety requirements is to model the CPS as a hybrid automaton and apply formal verification techniques. This hybrid automaton captures the evolution of both the discrete and continuous components of the CPS. A widely used sub-class of hybrid automata is linear hybrid automata where the continuous evolution of the system is given as solutions of linear differential equations. This talk will be about a new verification technique for linear hybrid automata.

In this talk, I will present a new development in dynamic analysis technique for linear hybrid system verification. In this technique, verification of an an n-dimensional system requires using a mere n+1 sample simulations. This technique greatly improves the scalability of verification. In this talk, I will present the basic algorithm for efficient dynamic analysis, its enhancements, and present verification results for systems with dimensions ranging from 10 - 10,000.