中文摘要：

系统实时性、安全性和可靠性等非功能属性是信息物理系统在诸多领域应用的关键因素。论文在分析CPS模型构建与分析验证中面临的挑战的基础上,提出了一种CPS行为建模与属性验证方法。该方法首先基于混成自动机对CPS的行为进行建模,然后将此模型转换为混合程序模型,最后在定理证明器KeYmaera中对HP模型的属性进行形式化验证。文中论述了行为模型描述语言的结构,建立了混成自动机模型与HP模型之间的转换规则,分析了模型转换的一致性。应用实例表明：该方法既能简单直观地描述CPS动态行为,又能对CPS的属性进行严格的形式化验证,且有效避免了形式化验证中的状态空间爆炸问题。

英文摘要：

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 consisten- cy 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 ex- plosion in formal verification effectively.