  Modeling and verifying real-world cyber-physical systems is challenging,
which is especially so for complex systems where manually modeling is
infeasible. In this work, we report our experience on combining model learning
and abstraction refinement to analyze a challenging system, i.e., a real-world
Secure Water Treatment system (SWaT). Given a set of safety requirements, the
objective is to either show that the system is safe with a high probability (so
that a system shutdown is rarely triggered due to safety violation) or not. As
the system is too complicated to be manually modeled, we apply latest automatic
model learning techniques to construct a set of Markov chains through
abstraction and refinement, based on two long system execution logs (one for
training and the other for testing). For each probabilistic safety property, we
either report it does not hold with a certain level of probabilistic
confidence, or report that it holds by showing the evidence in the form of an
abstract Markov chain. The Markov chains can subsequently be implemented as
runtime monitors in SWaT.
