Analyzing Neighborhoods of Falsifying Traces in Cyber-Physical Systems.

Ram Das Diwakaran, Sriram Sankaranarayanan, and Ashutosh Trivedi

We study the problem of analyzing falsifying traces of cyber-physical systems. Specifically, given a system model and an input which is a counterexample to a property of interest, we wish to understand which parts of the inputs are "responsible" for the counterexample as a whole. Whereas this problem is well known to be hard to solve precisely, we provide an approach based on learning from repeated simulations of the system under test.

Our approach generalizes the classic concept of "one-at-a-time" sensitivity analysis used in the risk and decision analysis commu- nity to understand how inputs to a system influence a property in question. Specifically, we pose the problem as one of finding a neighborhood of inputs that contains the falsifying counterexample in question, such that each point in this neighborhood corresponds to a falsifying input with a high probability. We use ideas from sta- tistical hypothesis testing to infer and validate such neighborhoods from repeated simulations of the system under test. This approach not only helps to understand the sensitivity of these counterexam- ples to various parts of the inputs, but also generalizes or widens the given counterexample by returning a neighborhood of coun- terexamples around it.

We demonstrate our approach on a series of increasingly com- plex examples from automotive and closed loop medical device domains. We also compare our approach against related techniques based on regression and machine learning.

Under review.
Email me for a copy of the paper © 2017.