UCLA

At a conference in March 2015, while advocating self-driving cars, Elon Musk, the chief executive officer of Tesla Motors, referred to (traditional) cars as “two-ton death machines”. The biggest promise of autonomous systems is the elimination of, or compensation for, the human-error factor. However, making sure that such systems which are designed by humans themselves, will behave as we expect them to do, is an unarguably challenging task. According to the RAND Corporation’s recent findings, demonstrating the failure rate of an autonomous vehicle to a particular degree of precision would take about 8.8 billion miles of test driving, which corresponds to 400 years with a fleet of 100 autonomous vehicles. This suggests that, as engineers, we need to develop alternative methods to excessive, brute force testing in order to fulfill the promise of bringing a safe product to the market. Moreover, in safety-critical applications such as self-driving cars, this promise should not only be filled, but it should be provably filled.

Most autonomous systems that are safety-critical also have a cyber-physical nature, meaning that they involve an interplay between cyber and physical components. In fact, the complex interactions between these components are what makes the design and verification of Cyber-Physical Systems (CPS) notoriously difficult. In this thesis, we look at the problem of correct design of CPS from two different angles. In the first chapter, 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. In the second chapter, 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. In the first chapter the problem setting is as follows: “Given a CPS and a desired specification in a formal language such as Linear Temporal Logic, can we synthesize provably correct controller software that will enforce the specification?” This question has already been addressed in the literature by bringing tools from computer science into the realm of control theory. However, for an arbitrary specification, the resulting methods are computationally expensive to a point that synthesis becomes intractable for large-scale systems. In this thesis, we address this problem by studying a certain class of specifications, which we call mode-target formulas. This class is small enough to lead to tractable algorithms, yet rich enough to answer interesting control problems. It is inspired by numerous control applications where there are multiple modes and corresponding (possibly multiple) targets to be reached and attained, hence the name. In Chapter 1, we formally define the mode-target formulas and then propose a solution methodology to perform controller synthesis, when the specifications are given in a mode-target setting.

In the second part of the thesis, we make use of a more traditional design tool for control theorists: Lyapunov functions. These functions serve as certificates for stability and thus have a significant role in the verification of dynamical systems. Even though stability analysis using Lyapunov techniques is a well-studied problem, the majority of the current literature only addresses it when the dynamics of the system is known and can be expressed in the form of a differential or difference equation. This creates a gap between the theory and practice because, for most industrial scale systems, there is no such simple representation of the underlying dynamics. Instead, what is available to the engineers in most scenarios is the ability to perform simulations. With this observation in mind, in Chapter 2, we take the first step to close this gap. In particular, provided that the underlying dynamics can be modeled as a switched linear system, we propose a technique to analyze the stability of the system by observing the response of the system to uniformly randomly sampled initial conditions.