Formal Synthesis and Data-driven Verification of Cyber-Physical Systems

Speaker: Ayca Balkan
Affiliation: Ph.D. Candidate - UCLA

Abstract:  The design and verification of Cyber-Physical systems (CPS) are notoriously difficult tasks due to the complex interactions between the cyber and physical components. In this talk, we look at the problem of correctly designing CPS from two different angles.

In the first part, we position ourselves within a correct-by-design paradigm, where the idea is not to spend a heroic effort in the verification phase, by ensuring that the design process itself leads to a certificate of correctness. We introduce a class of Linear Temporal Logic (LTL) specifications for which the problem of synthesizing controllers can be solved in polynomial time. The new class of specifications is an LTL fragment that we term Mode-Target and is inspired by numerous control applications where there are modes and corresponding (possibly multiple) targets for each mode. We formulate the problem of synthesizing a controller enforcing an MT specification as a game and provide a polynomial-time algorithm to solve this resulting game.

In the second part, we concentrate on generating correctness certificates for a completed design candidate. Here, with the challenges specific to the CPS in mind, we do not take a model based approach, but instead, a data driven one. Specifically, we address the problem of deciding stability of a “black-box” dynamical system (i.e., a system whose model is not known) from a set of observations. The only assumption we make on the black-box system is that it can be described by a switched linear system. We show that, for a given (randomly generated) set of observations, one can give a stability guarantee, for some level of confidence, with a trade-off between the quality of the guarantee and the level of confidence. Our results rely on geometrical analysis and combining chance-constrained optimization theory with stability analysis techniques for switched systems.

Biography:  Ayca Balkan received her B.S. degree in Electrical and Electronics Engineering from Middle East Technical University, Ankara, in 2010 and her M.S. degree in Electrical Engineering from the University of California at Los Angeles, in 2012. She was the recipient of the Preliminary Exam Fellowship in Signals & Systems area in 2012 and the Best Paper Award in ACM SIGBED Conference on Embedded Software (EMSOFT) in 2016. Her research interests include control theory, formal methods and cyber-physical systems.

For more information, contact Prof. Paulo Tabuada ()

Date(s) - May 31, 2017
10:30 am - 12:30 pm

E-IV Faraday Room #67-124
420 Westwood Plaza - 6th Flr., Los Angeles CA 90095