Probabilistic Conformance for Cyber-Physical Systems

TL;DR

This paper introduces a probabilistic conformance framework for cyber-physical systems using Signal Temporal Logic, providing statistical verification methods to ensure systems meet specifications with quantifiable confidence.

Contribution

It proposes a novel notion of probabilistic conformance for CPS and develops the first statistical verification methods for this purpose.

Findings

Verified conformance of Toyota powertrain startup times

Assessed settling times of automotive lane-keeping controllers

Analyzed voltage deviations in power grid systems

Abstract

In system analysis, conformance indicates that two systems simultaneously satisfy the same set of specifications of interest; thus, the results from analyzing one system automatically transfer to the other, or one system can safely replace the other in practice. In this work, we study the probabilistic conformance of cyber-physical systems (CPS). We propose a notion of (approximate) probabilistic conformance for sets of complex specifications expressed by the Signal Temporal Logic (STL). Based on a novel statistical test, we develop the first statistical verification methods for the probabilistic conformance of a wide class of CPS. Using this method, we verify the conformance of the startup time of the widely-used full and simplified model of Toyota powertrain systems, the settling time of model-predictive-control-based and neural-network-based automotive lane-keeping controllers, as well as the maximal voltage deviation of full and simplified power grid systems.