Most proposals for securing control systems are heuristic in nature, and while they increase the protection of their target, the security guarantees they provide are unclear. This paper proposes a new way of modeling the security guarantees of a Cyber-Physical System (CPS) against arbitrary false command attacks. As our main case study, we use the most popular testbed for control systems security. We first propose a detailed formal model of this testbed and then show how the original configuration is vulnerable to a single-actuator attack. We then propose modifications to the control system and prove that our modified system is secure against arbitrary, single-actuator attacks.

We address a classical identification problem that consists in estimating a vector of constant unknown parameters from a given linear input/output relationship. The proposed method relies on a network of gradient-descent-based estimators, each of which exploits only a portion of the input-output data. A key feature of the method is that the input-output signals are hybrid, so they may evolve in continuous time (i.e., they may flow), or they may change at isolated time instances (i.e., they may jump). The estimators are interconnected over a weakly-connected directed graph, so the alternation of flows and jumps combined with the distributed character of the algorithm introduce a rich behavior that is impossible to obtain using continuous- or discrete-time estimators. A condition of persistence of excitation in hybrid form ensures exponential convergence of the estimation errors. The proposed approach generalizes the existing centralized gradient-descent algorithms and yields relaxed sufficient conditions for (uniform-exponential) parameter estimation. In addition, we address the observation/identification problem for a class of hybrid systems with unknown parameters using a distributed network of adaptive observers/identifiers.

In this paper, we introduce tools to verify the satisfaction of temporal logic specifications using the until operator for hybrid dynamical systems. Hybrid dynamical systems are given in terms of differential and difference inclusions, which capture the continuous and discrete dynamics (or events), respectively. For such systems, conditional invariance and eventual conditional invariance are employed to characterize dynamical properties associated with the until operators. Sufficient conditions for the satisfaction of temporal logic specifications involving the until operator are provided by guaranteeing properties of the data defining the systems and the existence of barrier functions or Lyapunov-like functions. Examples illustrate the results throughout the paper.

Motivated by the safety problem, several definitions of reachability maps, for hybrid dynamical systems, are introduced. It is well established that, under certain conditions, the solutions to continuous-time systems depend continuously with respect to initial conditions. In such setting, the reachability maps considered in this paper are locally Lipschitz (in the Lipschitz sense for set-valued maps) when the right-hand side of the continuous-time system is locally Lipschitz. However, guaranteeing similar properties for reachability maps for hybrid systems is much more challenging. Examples of hybrid systems for which the reachability maps do not depend nicely with respect to their arguments, in the Lipschitz sense, are introduced. With such pathological cases properly identified, sufficient conditions involving the data defining a hybrid system assuring Lipschitzness of the reachability maps are formulated. As an application, the proposed conditions are shown to be useful to significantly improve an existing converse theorem for safety given in terms of barrier functions. Namely, for a class of safe hybrid systems, we show that safety is equivalent to the existence of a locally Lipschitz barrier function. Examples throughout the paper illustrate the results.

This paper investigates characterizations of safety in terms of barrier functions for hybrid systems modeled by hybrid inclusions. After introducing an adequate definition of safety for hybrid inclusions, sufficient conditions using continuously differentiable as well as lower semicontinuous barrier functions are proposed. Furthermore, the lack of existence of autonomous and continuous barrier functions certifying safety, guides us to propose, inspired by converse Lyapunov theorems for only stability, nonautonomous barrier functions and conditions that are shown to be both necessary as well as sufficient, provided that mild regularity conditions on the system's dynamics holds.

By this poster, we aim at presenting in a comprehensive manner our new results on safety characterization using barrier functions in the general context of hybrid systems. Roughly speaking, a dynamical system is said to be safe when the solutions starting from a given initial set never reach a given unsafe set. Barrier functions in this context constitute a qualitative methodological tool that avoid the computation of the system's solutions yet to determine if the safety property holds. According to literature, a barrier function candidate with respect to a given initial and unsafe sets is nonpositive on the initial set and strictly positive on the unsafe set. Such a barrier candidate becomes a certificate of safety provided that it satisfies some variational properties involving the system's dynamics at least in a specific region around its zero-sublevel set.