Uncertainty in safety-critical cyber-physical systems can be modeled using a finite number of parameters or parameterized input signals. Given a system specification in Signal Temporal Logic (STL), we would like to verify that for all (infinite) values of the model parameters/input signals, the system satisfies its specification. Unfortunately, this problem is undecidable in general. Statistical model checking (SMC) offers a solution by providing guarantees on the correctness of CPS models by statistically reasoning on model simulations. We propose a new approach for statistical verification of CPS models for user-provided distribution on the model parameters. Our technique uses model simulations to learn surrogate models , and uses conformal inference to provide probabilistic guarantees on the satisfaction of a given STL property. Additionally, we can provide prediction intervals containing the quantitative satisfaction values of the given STL property for any user-specified confidence level. We compare this prediction interval with the interval we get using risk estimation procedures. We also propose a refinement procedure based on Gaussian Process (GP)-based surrogate models for obtaining fine-grained probabilistic guarantees over sub-regions in the parameter space. This in turn enables the CPS designer to choose assured validity domains in the parameter space for safety-critical applications. Finally, we demonstrate the efficacy of our technique on several CPS models.

We describe data-driven algorithms, DaTaReach and DaTaControl, for reachability analysis and control of systems with a priori unknown nonlinear dynamics. The resulting algorithms provide provable performance guarantees while satisfying real-time constraints. To this end, they merge data from a single finite-horizon trajectory and, if available, various forms of side information derived from laws of physics and qualitative properties of the system. Specifically, DaTaReach constructs a differential inclusion that contains the unknown vector field. Then, it over-approximates the reachable set through interval Taylor-based methods applied to systems with dynamics described as differential inclusions. DaTaControl achieves near-optimal and convex-optimization-based control of the system through the computed over-approximations and the receding horizon framework. We empirically demonstrate that DaTaControl outperforms, in terms of optimality of the control and computation time, state-of-the-art control approaches based on system identification and contextual optimization. Finally, using the scenario of an F-16 aircraft diving towards the ground, we show how DaTaControl prevents a ground collision using only the measurements obtained during the dive and elementary laws of physics as side information.

We study the problem of falsifying reachability properties of real-time control software acting in a closed-loop with a given model of the plant dynamics. Our approach employs numerical techniques to simulate a plant model, which may be highly nonlinear and hybrid, in combination with symbolic simulation of the controller software. The state-space and input-space of the plant are systematically searched using a plant abstraction that is implicitly defined by ``quantization'' of the plant state, but never explicitly constructed. Simultaneously, the controller behaviors are explored using a symbolic execution of the control software. On-the-fly exploration of the overall closed-loop abstraction results in abstract counterexamples, which are used to refine the plant abstraction iteratively until a concrete violation is found. Empirical evaluation of our approach shows its promise in treating controller software that has precise, formal semantics, using an exact method such as symbolic execution, while using numerical simulations to produce abstractions of the underlying plant model that is often an approximation of the actual plant. We also discuss a preliminary comparison of our approach with techniques that are primarily simulation-based.

Specication guided falsication methods for hybrid systems have recently demonstrated their value in detecting design errors in models of safety critical systems. In specication guided falsication, the correctness problem, i.e., does the system satisfy the specication, is converted into an optimization problem where local negative minima indicate design errors. Due to the complexity of the resulting optimization problem, the problem is solved iteratively by performing a number of simulations on the system. Even though it is theoretically guaranteed that falsication methods will eventually find the bugs in the system, in practice, the performance of these methods, i.e., how many tests/simulations are executed before a bug is detected, depends on the specication, on the system and on the optimization method. In this paper, we define and utilize coverage metrics on the state space of hybrid systems in order to improve the performance of the falsication methods.

We present a search technique to falsify safety properties of hybrid systems that model a software system controlling a physical plant. Our approach takes as input (a) the controller code and (b) a plant model given as a black-box system that can be simulated for given inputs over finite time horizons. Our approach combines the symbolic execution of the controller software with an abstraction of the plant, which is discovered on-the-fly using simulations. This process is used to find abstract counterexamples to the safety properties of interest. The plant abstraction is then refined iteratively using the abstract counterexamples until a concrete violation is discovered. Empirical evaluation of our approach shows its promise in treating controller software, whose semantics are well-understood using formal techniques while using numerical simulations to produce abstractions of the underlying plant model, which is often an approximation of the actual plant.

In this paper, we present an approach for finding violations of safety properties of hybrid systems. Existing approaches search for complete system trajectories that begin from an initial state and reach some unsafe state. We present an approach that searches over segmented trajectories, consisting of a sequence of segments starting from any system state. Adjacent segments may have gaps, which our approach then seeks to narrow iteratively. We show that segmented trajectories are actually paths in the abstract state graph obtained by tiling the state space with cells. Instead of creating the prohibitively large abstract state graph explicitly, our approach implicitly performs a randomized search on it using a scatter-and-simulate technique. This involves repeated simulations, graph search to find likeliest abstract counterexamples, and iterative refinement of the abstract state graph. Finally, we demonstrate our technique on a number of case studies ranging from academic examples to models of industrial-scale control systems.