面向CPS时空性质验证的混成AADL建模与模型转换方法

Hybrid AADL Modeling and Model Transformation for CPS Time and Space Properties Verification

随着信息物理融合系统CPS(cyber physical system)研究的深入,CPS的安全性问题越来越受到人们的广泛关注,如何验证CPS时空不一致的安全性问题已经成为研究热点.针对该问题,提出了面向CPS时空性质验证的混成AADL(architecture analysis&design language)建模与模型转换方法.首先,扩展AADL行为附件的时空描述能力,提出了混成AADL(hybrid architecture analysis&design language),用于建模CPS的时空性质;其次,在进程代数中引入微分方程以及位置描述,提出了HP-TCSP,能够验证CPS的时空性质;再次,通过模型转换,将混成AADL转换为HP-TCSP,从而可以将混成AADL描述的CPS模型在HP-TCSP中进行时空一致性验证;最后,通过一个飞机避撞系统实例,验证该方法的有效性.

With the in-depth research of CPS(cyber physical system),the security problems of CPS are gradually attracted extensive attention.How to verify the security of space and time inconsistency of CPS has become a research hot spot.A hybrid AADL(architecture analysis&design language)modeling and model transformation method for CPS is proposed to solve this problem.Firstly,the time and space description capability of AADL behavior annex is extended,and Hybrid AADL(hybrid architecture analysis&design language)is proposed.Secondly,the differential equation and the position description are introduced into the process algebra.Thirdly,the hybrid AADL is transformed into HP-TCSP.Finally,the effectiveness of the proposed method is verified by an example of aircraft anti-collision system.