Formal Verification of Robustness Properties of Hybrid Control Systems
Tuesday, April 11, 2017
4-5 p.m., Avery 115
3:30 p.m., Avery 348
Pavithra Prabhakar, DoctorateAssociate Professor, Kansas State University
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
Pavithra Prabhakar is an associate professor in the Department of Computer Science at Kansas State University. She holds a Michelle Munson-Serban Simu Keystone Research Faculty Scholarship from the College of Engineering. 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, an NSF CAREER Award and an ONR Young Investigator Award.