Closed-loop Model Checking of Cyber-Physical Systems

Ensuring the safety and efficacy of Cyber-Physical Systems (CPS) is challenging due to the large variability of their physical environment. Model checking has been widely adopted for CPS validation. However, due to the lack of knowledge in formal methods, users of model checker often create environment models that are either too specific to capture the variability of the environment, or too abstract to provide interpretable counter-examples. In this paper, a domain-independent framework for environment model abstraction and refinement is proposed to provide interpretable counter-examples while ensuring coverage of environment behaviors. With the framework, system developers and application domain experts can rigorously and effectively utilize model checking without being an expert in formal methods. A simple case study in the automotive domain is used to demonstrate the feasibility of the framework and the soundness of our domain-independent abstraction rules.