Correct-by-Construction Control Adaptation against Sensing, Model, and Information Uncertainty

Abstract

The theory of formal methods had a profound effect on computer science. By providing tools that can verify a program’s correctness or generate software that is “correct-by-construction,” Formal Methods made it much easier to design safer, bug-free code for computer systems. Safe, bug-free code is not only helpful in pure software systems, but also in systems that interact with and manipulate the world. Unfortunately, these so-called Cyber-Physical Systems (CPSs) have limitations or considerations that prevent many of the formal methods tools from being immediately applied to them. Of the many limitations that prevent Formal Methods from being applied to Cyber-Physical Systems, this dissertation discusses three types: sensing, modeling, and information limitations.

First, this dissertation develops a method for overcoming a practical sensing limitation called “missing data.” Missing data refers to a phenomena where some data that is important to the CPSs safety is lost either in transmission or during sensing. This work provides a method for guaranteeing safety of a CPS experiencing missing data during a reachability task. Specifically, we define a linear program that is feasible if and only if an adaptive controller exists that is guaranteed to achieve the reachability task subject to missing data. The adaptive controller is composed of prefix-constrained linear controllers with a simple switching rule between them and can be optimized with respect to a convex objective function.

Second, this dissertation develops a method for overcoming the limitations in our ability to model CPSs. Often, a single model of the CPS is not known a priori but a family of potential models is known. To guarantee that our system is safe while accomplishing a reachability task and with only a family of models known a priori, this work provides a bilinear optimization-based method which can guarantee task satisfaction despite this initial model uncertainty. Each model can be incorporated into an optimization using a consistency set, which is similar to a reachable set but contains additional model information. The consistency set is used to determine which actions will discriminate (or reveal information about the true, linear mode of the system) a priori and thus analyzes the trade-offs of discriminating actions and other tasks (such as reachability of a target region or minimization of a cost). The controller design problem is defined as a bilinear optimization. Rather than constructing this bilinear optimization problem from scratch, a method is presented for translating Linear Temporal Logic with the epistemic knowledge operator (KLTL) formulae into bilinear optimization problems.

Thirdly, this dissertation develops a method for overcoming the limited ability of a single CPS to make safe actions when part of a large collection of connected CPSs. The proposed method decomposes the problem of guaranteeing the safety of a collection of CPSs into a series of smaller problems for each individual agent using the framework of the inter-triggering hybrid automaton (ITHA). Under this framework, the problem can be solved by finding self-safe actions (actions that an agent knows should be safe under its own dynamics) along with responsible actions (actions that will not cause problems for others that this agent is “responsible for”).