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

Behavior Modeling and Attribute Validation of Cyber-Physical System(CPS)Based on Hybrid Automata

作　　者：拓明福[1,2] 周兴社[1] 李嘉林[2] 李辉[2] 

机构地区：[1]西北工业大学计算机学院,西安710129 [2]空军工程大学理学院,西安710051

出　　处：《空军工程大学学报（自然科学版）》2016年第3期40-44,共5页Journal of Air Force Engineering University(Natural Science Edition)

基　　金：国家自然科学基金(61472443)

摘　　要：系统实时性、安全性和可靠性等非功能属性是信息物理系统在诸多领域应用的关键因素。论文在分析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.

关 键 词：信息物理系统 模型验证 混成自动机 混合程序 模型转换 

分 类 号：TP393[自动化与计算机技术—计算机应用技术]