Automatic Abstraction for Verification of Cyber-Physical Systems

Verification of cyber-physical systems is complicated by both their heterogeneous nature as well as their sheer complexity. Cyber-physical systems include hardware, software, and physical  environment, so a formal model must integrate all of these concerns. Unfortunately, modeling a system with all of its details results in state explosion. Therefore, it is necessary to automatically abstract the model to include only those details necessary to verify the  property of interest. Constructing such a model is the focus of this work.