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

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. We also illustrate through examples how this compositional approach significantly reduces the time required for the construction of abstractions. 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. We illustrate, through different examples, how this lazy approach significantly reduces the total time required for the synthesis of correct-by-construction controllers. In addition to exploiting structure and lazy synthesis, we also discuss possible future extensions to these two approaches