Cyber/Physical Co-verification for Developing Reliable Cyber-physical Systems

Cyber-Physical Systems (CPS) tightly integrate cyber and physical components and transcend discrete and continuous domains. It is greatly desired that the physical components being controlled and the software implementation of control algorithms can be verified together. We present an efficient approach to reachability analysis of Hybrid Automata Pushdown System (HAPS) models for cyber/physical co-verification of CPS. We have realized this approach and applied it to real-world control systems. The evaluation has shown that HAPS is an effective model for co-verification of CPS and our approach has major potential in verifying system-level properties of CPS, therefore improving the reliability of CPS.