intro.tex

Simulation-driven model-based development is rapidly becoming the
preferred paradigm for developing embedded control software in an
industrial context.  Tools like \SIMULINK are often used to create
models of closed-loop dynamical systems, \ie, a plant model of the
physical systems that we wish to control, and a model for the embedded
controllers.  Automatic approaches for testing the safety and
performance of such closed-loop systems largely focus on guided
testing using numerical simulations
\cite{annpureddy2011s,donze2010breach,deshmukh2015stochastic,dreossi2015efficient,akazaki}.
On the other hand, a common approach taken in formal verification
approaches for hybrid and timed systems is to model such closed-loop
systems as restricted classes of dynamical systems such as those with
constant, affine \cite{frehse2011spaceex}, or polynomial
\cite{chen2015reachability} dynamics. Constructing such conservative
abstractions of real-world closed-loop systems involves a difficult
tradeoff between keeping the computed abstraction small in size but
high in fidelity.

In this paper, we wish to find inputs to the system and system initial
conditions that falsify safety properties of effectively black-box
systems, \ie, systems where the dynamics are highly complex, or not
expressed in a closed-form. We thus investigate a falsification
approach that operates on an on-the-fly abstraction of the system
constructed by assuming that the system dynamics have a certain form.
Our approach has two main steps: In the first step, we learn a
piece-wise {\em relational model} from simulations of the given
dynamical system. In the second step, we leverage symbolic techniques
to exhaustively analyze the model learned in the first phase. We
remark that the approach we propose is neither sound nor complete: a
violation found by our technique may not exist in the original system,
and our technique may miss violations that exist in the original
system. A fair question is: why is such a technique useful? There are
two perspectives from which we can answer this question.

In many settings, we may not have a physics-based model derived from
first principles, but may just have time-series data of the system
behavior. In such a setting, a data-driven model allows us to
generalize individual time-series behaviors. But, there are several
approaches in the literature to perform data-driven modeling; e.g.,
system identification techniques that learn dynamic models from data
\cite{ljung1999system}, auto-regressive models for forecasting
\cite{wei1994time}, bounded-error hybrid systems identification
methods \cite{bemporad2003greedy,bemporad2005bounded}, clustering
based methods \cite{ferrari2003clustering}, methods to identify
piecewise affine dynamics \cite{paoletti2007identification}, and
machine learning techniques that learn static or dynamic models from
data
\cite{narendra1990identification,lu2009linear,juloski2005bayesian}.
Why then do we need a new modeling technique? The answer to this
question lies in our goal for the second step, \ie, symbolic analysis
of the learned model. For this step, we need to have models that can
be digested by existing symbolic tools, which is harder to do with
some of the aforementioned heavier data-driven modeling methods.
Hence, we use a lighter flavor of data-driven modeling such as the one
proposed for learning relational models from data
\cite{zutshi2012timed,sankaranarayanan2011relational}. By learning a
{\em kernelized relational model}, \ie, essentially a discrete-time
dynamical system with a chosen form for the dynamics, we can use
software analysis approaches such as bounded model checking assisted
by SMT solvers and linear programming solvers.

The other perspective for our technique is that we are often faced
with black-box models, where symbolic analysis is rather challenging.
We note that the ultimate goal is to find violations of safety
properties in the {\em actual embedded control system}, and not, per
se, in the model. The aphorism attributed to mathematician George E.P.
Box is quite apt for our context, and bears worth repeating,  ``all
models are wrong, some models are useful.'' We can sidestep analyzing
a highly complex model by approximating its behavior with a simpler
relational model, which in turn can give us promising tests to run on
the actual system. This gives our technique intrinsic value as a
debugging tool.

In \cite{zutshi2014multiple}, the authors investigate an on-the-fly
abstraction technique that is close to the approach we propose.  This
approach use an existential abstraction of the state-space of a given
hybrid dynamical system. The abstract model learned can be viewed as a
discrete-time transition system, where states of the transition system
are cells in a tiling-based abstraction, and an edge between two cells
indicates a concrete transition between the states of the actual
system contained in the cell.  A key difference in this paper is that
the model being learned in addition to being such a transition system
is that it is now enriched with labels on the states and transitions.
These labels capture {\em relations} between source and destination
states. Thus an edge between two cells can now represent the {\em
guard} region within the cell where the source states lie, and the
(symbolic) {\em update} relation between the destination and the
source states.  The relations that we learn depend on user-specified
{\em kernels}, \ie, if the user specifies that the relations should be
linear, we can use techniques such as linear regression or convex hull
computation to obtain the update and guard relations respectively.
Other kernels such as polynomials can also be included.  The relations
discovered approximate locally observed behaviors, and the resulting
kernelized transition system can be interpreted as a symbolic,
discrete labeled transition system. We can apply time-bounded model
checking to find counterexamples to bounded safety properties on such
a system. A counterexample if found, can indicate the presence of a
violation in the system.  We can then use this counterexample to guide
the search towards a violation in the original system. 

We remark that our work focusses on building piecewise relational
models, and is unrelated to work on analyzing dynamical systems that
have piecewise-affine (PWA) vector fields. Techniques to analyze PWA
dynamical systems using bisimulation relations translate the system
into a non-deterministic infinite state transition system that is
required to be an over-approximation of the original system and use
model checking approaches to verify them \cite{asarin2000approximate}.

% Related approaches using bisimulation relations
%\cite{pappas2003bisimilar,tabuada2006linear, yordanov2007model} have
% interesting parallels with the work presented here.

The layout of the paper is as follows: In Section~\ref{sec:scam}, we
review the discrete-time on-the-fly transition system abstraction
introduced by \cite{zutshi2014multiple}.  We show how to enrich this
abstraction to kernelized transition systems in
Section~\ref{sec:scamr}.  We show how such systems can be analyzed
using symbolic bounded model checking in Sec.~\ref{sec:bmc}.  We
present an approach to refine the relational transition systems in
Sec.~\ref{sec:rel-mod}, and present experimental validation of our
technique on a few examples systems in Section~\ref{sec:res}.