软件学报

作者：陈小颖，祝义，赵宇，王金永

单位：陈小颖，江苏师范大学 计算机科学与技术学院, 江苏 徐州 22111611,祝义，江苏师范大学 计算机科学与技术学院, 江苏 徐州 22111602,赵宇，江苏师范大学 计算机科学与技术学院, 江苏 徐州 22111603,王金永，南京航空航天大学 计算机科学与技术学院, 江苏 南京 21110604

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

基金：国家自然科学基金（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中进行时空一致性验证；最后，通过一个飞机避撞系统实例，验证该方法的有效性.

来源：2021年第6期

《软件学报》期刊编辑部

查看软件学报杂志2021年第6期