A Unified Modeling and Verifying Framework for Cyber Physical Systems

In CPS (cyber-physical systems), computation is integrated with physical processes, computer system is used to monitor and interact with the physical world to realize maximization of benefit and usage. The model and verification for cyber physical systems are two important and challenge problems because CPS has not only heterogeneous nature but also very complicated structure and relationships among its components. In this paper, a unified framework is proposed to model and verify CPS, where CPS is modeled in forms of HybridUML models, then these HybridUML models are transformed to different operating models of Differential Dynamic Logic (DL), and finally some CPS properties are specified using DDL equations and verified using DDL reasoning rules.