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

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

作　　者：陈小颖 祝义[1] 赵宇[1] 王金永 CHEN Xiao-Ying;ZHU Yi;ZHAO Yu;WANG Jin-Yong(School of Computer Science and Technology,Jiangsu Normal University,Xuzhou 221116,China;College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 211106,China)

机构地区：[1]江苏师范大学计算机科学与技术学院,江苏徐州221116 [2]南京航空航天大学计算机科学与技术学院,江苏南京211106

出　　处：《软件学报》2021年第6期1779-1798,共20页Journal of Software

基　　金：国家自然科学基金(62077029);徐州市应用基础研究计划(KC19004);江苏省研究生科研创新计划(KYCX20_2380);江苏省研究生科研创新计划(KYCX20_2384)。

摘　　要：随着信息物理融合系统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.

关 键 词：信息物理融合系统 时空性质 进程代数 AADL 形式化验证 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]