  In this paper, we propose conformal inference based approach for statistical
verification of CPS models. Cyber-physical systems (CPS) such as autonomous
vehicles, avionic systems, and medical devices operate in highly uncertain
environments. This uncertainty is typically modeled using a finite number of
parameters or 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. {\em 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 {\em surrogate models}, and uses {\em 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 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.
