Environment Modeling During Model Checking of Cyberphysical Systems

A domain-independent framework for the abstraction and refinement of the environment model is proposed to provide interpretable counterexamples while ensuring coverage of environment behaviors. A simple case study in the automotive domain is used to demonstrate the feasibility of the framework.