  This paper employs correct-by-construction control synthesis, in particular
controlled invariant set computations, for falsification. Our hypothesis is
that if it is possible to compute a "large enough" controlled invariant set
either for the actual system model or some simplification of the system model,
interesting corner cases for other control designs can be generated by sampling
initial conditions from the boundary of this controlled invariant set.
Moreover, if falsifying trajectories for a given control design can be found
through such sampling, then the controlled invariant set can be used as a
supervisor to ensure safe operation of the control design under consideration.
In addition to interesting initial conditions, which are mostly related to
safety violations in transients, we use solutions from a dual game, a
reachability game for the safety specification, to find falsifying inputs. We
also propose optimization-based heuristics for input generation for cases when
the state is outside the winning set of the dual game. To demonstrate the
proposed ideas, we consider case studies from basic autonomous driving
functionality, in particular, adaptive cruise control and lane keeping. We show
how the proposed technique can be used to find interesting falsifying
trajectories for classical control designs like proportional controllers,
proportional integral controllers and model predictive controllers, as well as
an open source real-world autonomous driving package.
