Page 205 - 《软件学报》2021年第6期

软件学报 ISSN 1000-9825, CODEN RUXUEW E-mail: jos@iscas.ac.cn
Journal of Software,2021,32(6):1779−1798 [doi: 10.13328/j.cnki.jos.006249] http://www.jos.org.cn
©中国科学院软件研究所版权所有. Tel: +86-10-62562563

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

1
1
1
陈小颖 , 祝 义 , 赵 宇 , 王金永 2
1
(江苏师范大学 计算机科学与技术学院,江苏 徐州 221116)
2 (南京航空航天大学 计算机科学与技术学院,江苏 南京 211106)
通讯作者: 祝义, E-mail: zhuy@jsnu.edu.cn

摘 要: 随着信息物理融合系统 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 中进行时空一致性验证;最后,通过一个飞机避撞系
统实例,验证该方法的有效性.
关键词: 信息物理融合系统;时空性质;进程代数;AADL;形式化验证
中图法分类号: TP311

中文引用格式: 陈小颖,祝义,赵宇,王金永.面向 CPS 时空性质验证的混成 AADL 建模与模型转换方法.软件学报,2021,32(6):
1779−1798. http://www.jos.org.cn/1000-9825/6249.htm
英文引用格式: Chen XY, Zhu Y, Zhao Y, Wang JY. Hybrid AADL modeling and model transformation for CPS time and space
properties verification. Ruan Jian Xue Bao/Journal of Software, 2021,32(6):1779−1798 (in Chinese). http://www.jos.org.cn/1000-
9825/6249.htm

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

1
1
1
CHEN Xiao-Ying , ZHU Yi , ZHAO Yu , WANG Jin-Yong 2
1 (School of Computer Science and Technology, Jiangsu Normal University, Xuzhou 221116, China)
2 (College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing 211106, China)
Abstract: 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.

∗ 基金项目: 国家自然科学基金(62077029); 徐州市应用基础研究计划(KC19004); 江苏省研究生科研创新计划(KYCX20_
2380); 江苏省研究生科研创新计划(KYCX20_2384)
Foundation item: National Natural Science Foundation of China (62077029); Applied Basic Research Program of Xuzhou
(KC19004); the Graduate Science Research Innovation Program of Jiangsu Province (KYCX20_2380); the Graduate Science Research
Innovation Program of Jiangsu Province (KYCX20_2384)
本文由“形式化方法与应用”专题特约编辑姜宇副教授推荐.
收稿时间: 2020-08-30; 修改时间: 2020-10-26; 采用时间: 2020-12-19; jos 在线出版时间: 2021-02-07