基于混成自动机的CP S行为建模与属性验证

摘要

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