Events Calendar

Center for Cyber-Physical Systems and Internet of Things and Ming Hsieh Institute for Electrical Engineering Joint Seminar Series on Cyber-Physical Systems

Speaker: Pavithra Prabhakar, Associate Professor, Kansas State University

Talk Title: Formal Verification of Robustness Properties of Cyber-Physical Systems

Abstract: Cyber-physical systems (CPSs) consist of complex systems that combine control, computation and communication to achieve sophisticated functionalities as in autonomous driving in driverless cars and automated load balancing in smart grids. The safety criticality of these systems demands strong guarantees about their correct functioning. Formal verification is an area of computer science that deals with rigorous and automated methods for correctness analysis based on mathematical models of systems and correctness specifications. In this talk, we present an overview of our work on formal verification techniques for cyber-physical systems analysis using the framework of hybrid systems. Hybrid systems capture an important feature of CPSs, namely, mixed discrete-continuous behaviors that arise due to the interaction of complex digital control software (discrete elements) with physical systems (continuous elements).

We will focus on the formal verification of a fundamental property in control design, namely, stability. Stability is a robustness property that capture notions such as small perturbations to the initial state or input to a system result in only small variations in the behavior of the system. We will present a novel algorithmic approach to stability analysis based on model-checking and abstraction-refinement techniques. We highlight the technical challenges in the development of an algorithmic framework for stability analysis owing to the robustness aspect. We will present experimental results using our tool AVERIST (Algorithmic VERifier for STability), that illustrate the practical benefits of the algorithmic approach as compared to well-known deductive methods for automated verification of stability based on Lyapunov functions. Finally, we will present some future research directions including automated design of hybrid control systems and formal analysis of hybrid systems in the presence of uncertainties.


Biography: Pavithra Prabhakar is an associate professor in the Department of Computer Science and Peggy and Gary Edwards Chair in Engineering at the Kansas State University. She obtained her doctorate in Computer Science and a masters in Applied Mathematics from the University of Illinois at Urbana-Champaign, followed by a CMI postdoctoral fellowship at the California Institute of Technology. Her main research interest is in formal analysis of cyber-physical systems with emphasis on both foundational and practical aspects related to automated and scalable techniques for verification and synthesis of hybrid systems. She is the recipient of a Marie Curie Career Integration Grant from the EU, a National Science Foundation CAREER Award and an Office of Naval Research Young Investigator Award.

Host: Paul Bogdan

Location: Hughes Aircraft Electrical Engineering Center (EEB) - 132

Audiences: Everyone Is Invited

Contact: Estela Lopez