Contributions Toward Scalability of Correct-by-Construction Control Software Synthesis

Speaker: Omar Hussien
Affiliation: Ph.D. Candidate - UCLA

Abstract: As cyber-physical systems (CPS) become more complex, the verification of CPS control software becomes notoriously challenging. One way to alleviate the need for verification is to adopt a correct-by-construction approach. By synthesizing the control software along with a proof of correctness, the correct-by-construction approach eliminates, or greatly reduces, the need for verification. A common correct-by-construction approach is based on the computation of a finite-state abstraction of the control system. Given a specification expressed in a formal language such as temporal logic, a controller that enforces this specification on the abstraction is first synthesized and then refined to a controller enforcing the same specification on the original system. Despite the promise of correct-by-construction control software, this design methodology is not yet widely applicable as the computation of abstractions scales exponentially with the number of variables in the differential equation model of the system to be controlled. In this thesis, we discuss two approaches to mitigate this problem: 1) exploiting system structure and 2) lazy controller synthesis.

In the first part of the thesis, we show how system structure can be exploited by discussing the class of partially feedback linearizable control systems. We show how the linearized part and the zero dynamics can be independently abstracted and subsequently composed to obtain an abstraction of the original continuous system. Moreover, we discuss how this approach can be further generalized to a larger class of systems.

In the second part of the thesis, we present a lazy controller synthesis approach to tackle the lack of scalability of control software synthesis. Instead of synthesizing a controller using a precomputed abstraction of the full system, fragments of the abstraction are computed lazily, as needed, to synthesize a controller for various specifications in temporal logic.

In addition to exploiting structure and lazy synthesis, we also discuss possible future extensions to these two approaches.

Biography: Omar Hussien received his B.S. and M.S. in Computer Engineering in 2009 and 2012, respectively, from Cairo University in Egypt. Before joining UCLA, he was an Assistant Lecturer in the Computer Engineering Department at Cairo University and a part-time Digital Design Engineer at Si-Ware Systems, Egypt.

For more information, contact Prof. Paulo Tabuada ()

Date(s) - Jul 05, 2018
2:00 pm - 4:00 pm

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