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

• 作 者: 陈小颖 祝义 赵宇 王金永
• 机 构: 江苏师范大学计算机科学与技术学院,南京航空航天大学计算机科学与技术学院
• 出 处: 软件学报
• 发表日期: 2021年6期
• 关键词: 信息物理融合系统 时空性质 进程代数 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),用于建