A Unified Modeling and Verifying Framework for Cyber Physical Systems

In CPS (cyber-physical systems), computationis integrated with physical processes, computer system isused to monitor and interact with the physical world to realize maximization of benefit and usage. The mode land 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 mode land verify CPS, where CPS is modeled in forms of Hybrid UML models, then these Hybrid UML 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.