摘要
随着信息物理融合系统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.
作者
陈小颖
祝义
赵宇
王金永
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)
出处
《软件学报》
EI
CSCD
北大核心
2021年第6期1779-1798,共20页
Journal of Software
基金
国家自然科学基金(62077029)
徐州市应用基础研究计划(KC19004)
江苏省研究生科研创新计划(KYCX20_2380)
江苏省研究生科研创新计划(KYCX20_2384)。
关键词
信息物理融合系统
时空性质
进程代数
AADL
形式化验证
CPS(cyber physical system)
time and space properties
process algebra
AADL
formal verification
