  Software verification may yield spurious failures when environment
assumptions are not accounted for. Environment assumptions are the expectations
that a system or a component makes about its operational environment and are
often specified in terms of conditions over the inputs of that system or
component. In this article, we propose an approach to automatically infer
environment assumptions for Cyber-Physical Systems (CPS). Our approach improves
the state-of-the-art in three different ways: First, we learn assumptions for
complex CPS models involving signal and numeric variables; second, the learned
assumptions include arithmetic expressions defined over multiple variables;
third, we identify the trade-off between soundness and informativeness of
environment assumptions and demonstrate the flexibility of our approach in
prioritizing either of these criteria.
  We evaluate our approach using a public domain benchmark of CPS models from
Lockheed Martin and a component of a satellite control system from LuxSpace, a
satellite system provider. The results show that our approach outperforms
state-of-the-art techniques on learning assumptions for CPS models, and
further, when applied to our industrial CPS model, our approach is able to
learn assumptions that are sufficiently close to the assumptions manually
developed by engineers to be of practical value.
