Nonfunction attribute such as realtime, security, and reliability, etc. is a key factor in cyberphysical systems applied to many areas. On the basis of analyzing CPS modeling and verification, a CPS behavior modeling and attribute verification is proposed in this paper. In this method, three steps are as follows: (1) to model the behavior of CPS based on hybrid automata; (2) to convert this model to HP model; (3) to verify the HP model in KeYmarera. The structure of behavior model language is introduced. Rules of converting hybrid automata model to hybrid program (HP) model are established. The consistency of the conversion is analyzed. The result shows that this method can depict the behavior of CPS simply and intuitively, and can also verify the properties of CPS strictly. By doing so, this avoids state space explosion in formal verification effectively.