| 面向CPS时空性质验证的混成AADL建模与模型转换方法 |
| |
| 引用本文： | 陈小颖,祝义,赵宇,王金永.面向CPS时空性质验证的混成AADL建模与模型转换方法[J].软件学报,2021,32(6):1779-1798. |
| |
| 作者姓名： | 陈小颖 祝义 赵宇 王金永 |
| |
| 作者单位： | 江苏师范大学 计算机科学与技术学院, 江苏 徐州 221116;南京航空航天大学 计算机科学与技术学院 南京 211106 |
| |
| 基金项目： | 国家自然科学基金（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中进行时空一致性验证；最后通过一个飞机避撞系统实例，验证该方法的有效性.
|
| 关 键 词： | 信息物理融合系统 时空性质 进程代数 AADL 形式化验证 |
| 收稿时间： | 2020/8/30 0:00:00 |
| 修稿时间： | 2020/10/26 0:00:00 |
Hybrid AADL Modeling and Model Transformation for CPS Time and Space Properties Verification |
| |
| CHEN Xiao-Ying,ZHU Yi,ZHAO Yu,WANG Jin-Yong.Hybrid AADL Modeling and Model Transformation for CPS Time and Space Properties Verification[J].Journal of Software,2021,32(6):1779-1798. |
| |
| Authors: | CHEN Xiao-Ying ZHU Yi ZHAO Yu WANG Jin-Yong |
| |
| Affiliation: | 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 |
| |
| Abstract: | |
| |
| Keywords: | CPS time and space properties Process Algebra AADL Formal Verification |
|
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载全文 |
