Design and Verification of Resilient Cyber-Physical Systems: A Satisfiability Modulo Convex Programming Approach

Seminar | March 13 | 4-5 p.m. | Cory Hall, DOP Center Conference Room (540A/B)

 Yasser Shoukry, Assistant Professor, University of Maryland, College Park

 Electrical Engineering and Computer Sciences (EECS)

Cyber-physical systems (CPSs) result from the integration of both computation and communication with physical processes. The behavior of CPSs is defined by the cyber and the physical parts of the system. Due to their massive deployment in safety-critical areas, including transportation, health-care, and infrastructure, CPSs have tight requirements in terms of safety, reliability, and security. Moreover, due to their heterogeneous nature, both the analysis and the design of CPSs increasingly require methods and tools that can efficiently reason about the interaction between discrete models (used to describe embedded software components), and continuous models (used to describe physical processes). In this respect, a central difficulty is the very different nature of the mathematical tools used to analyze discrete dynamics (e.g., combinatorics) and continuous dynamics (e.g., real analysis). This difficulty is exacerbated by complex, high-dimensional systems, where a vast discrete/continuous space must be searched under constraints that are often nonlinear.

I will argue that several problems that arise in different CPS problems (including security, high-assurance, verification) have something in common. Regardless of their heterogeneous nature, they can be formulated as a feasibility problem for a type of formula we call as monotone Satisfiability Modulo Convex programming (or SMC for short). I will present then a new SMC decision procedure that uses a lazy combination of Boolean satisfiability solving and convex programming to provide a satisfying assignment or determine if the formula is unsatisfiable. I will finish by showing, through multiple experimental results, the real-time and the resilience performance of the proposed SMC framework within different applications of resilient cyber-physical systems.

Bio: Yasser Shoukry is an Assistant Professor in the Department of Electrical and Computer Engineering at the University of Maryland, College Park where he leads the Resilient Cyber-Physical Systems Lab. He received his Ph.D. in Electrical Engineering from the University of California, Los Angeles in 2015. Between September 2015 and July 2017, Yasser was a joint postdoctoral researcher at UC Berkeley, UCLA, and UPenn. His current research focuses on the design and implementation of resilient cyber-physical systems and IoT. His work in this domain was recognized by the NSF CAREER Award, the Best Demo Award from the International Conference on Information Processing in Sensor Networks (IPSN) in 2017, the Best Paper Award from the International Conference on Cyber-Physical Systems (ICCPS) in 2016, and the Distinguished Dissertation Award from UCLA EE department in 2016. In 2015, he led the UCLA/Caltech/CMU team to win the NSF Early Career Investigators (NSF-ECI) research challenge. His team represented the NSF-ECI in the NIST Global Cities Technology Challenge, an initiative designed to advance the deployment of Internet of Things (IoT) technologies within a smart city.

 Jean Richter, Academic HR Analyst, EECS Department, UC Berkeley #223 Cory Hall, Berkeley, CA 94720-1770, jeanrichter@berkeley.edu, 5106438208