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

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

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

Real-time, security and reliability are key factors affecting the application of CPS in many areas. A software architecture for CPS behavior modeling and attribute verification is proposed in this paper. In this architecture, we do three things: (1)modeling of the behavior of CPS based on hybrid automata; (2)conversion of this model to HP model ;(3) validation of the model. The structure of behavior model language is introduced. Rules which convert hybrid automata model to hybrid program(HP) model are given. This architecture can depict the characteristics of CPS well and can avoid state space explosion in formal validation.