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

1780 Journal of Software 软件学报 Vol.32, No.6, June 2021

Key words: CPS (cyber physical system); time and space properties; process algebra; AADL; formal verification

近年来,随着云计算、物联网与 5G 技术的快速发展,信息物理融合系统 CPS(cyber physical system)的应用
已经覆盖到我们生产生活的各个方面,其安全性问题也受到了广泛关注,尤其在很多安全系数较高的 CPS 场景
[1]
中,如飞机飞行控制系统,汽车控制系统,铁路控制系统等,系统的安全性验证 显得尤为重要.2016 年,一名司机
驾驶特斯拉 Model S 在自动导航模式下与一辆牵引挂车碰撞发生车祸身亡.究其原因:是在明亮的晴朗天气,牵
引挂车白色车体反光严重,汽车组件失灵未能识别而导致碰撞.2018 年,Uber 自动车在夜间环境中未能通过阴
[2]
影识别行人 ,从而导致撞击行人致死.这些安全关键的 CPS 系统产生错误,将造成严重的后果.因此,需要一种
安全性验证的方法对 CPS 系统安全性进行保证.而时间与空间属性是保证安全性的关键因素.所以,如何验证在
复杂的运行环境下 CPS 的时空一致性以保障 CPS 的安全性,是当前面临的挑战.
体系结构分析与设计语言(hybrid architecture analysis & design language,简称 AADL)是于 2004 年由自动化
[3]
工程师学会发布的建模语言 ,AADL 自提出以来便受到广泛关注.该语言基于系统构件层次化的结构设计方
法,能够以统一的方式对硬件与软件进行抽象建模,支持高度可演化系统的开发.AADL 语言能提供所需构件之
间的分层功能,同时支持文本和图形化的描述方式从而快速建模,其行为附件支持对性质的扩展,在 CPS 建模过
程中具有很高的灵活性和实用性.因此,AADL 目前已经成为许多学者对 CPS 建模的首选语言,且在 CPS 领域广
泛使用.文献[4]基于 AADL 对云信息物理融合系统建模,进行数据质量分析、实时性能分析和资源消耗分析;
文献[5]将模型检查集成到设计过程中,根据 AADL 中的高级规范生成定时自动机模型,从而将模型检查技术集
成到 CPS 设计过程中.然而,AADL 并没有足够的能力描述 CPS 的性质以及异构特性与连续行为等特点.因此,
相关学者在 AADL 语言上进行相应的扩展,从而更好地对 CPS 进行研究.文献[6]构造了新的 AADL 子语言
AADL+,描述 CPS 连续行为以及网络组件和物理组件之间的交互;文献[7]提出了基于扩展 AADL 的 CPS 集成
建模框架描述方法,实现计算实体、物理实体和交互实体的统一描述;文献[8]将 AADL 与 Simulink/Stateflow 结
合,提供了统一的图形化协同建模形式,支持 CPS 软件、硬件和物理这 3 个角度统一设计;文献[9]针对 AADL
嵌入式系统体系结构进行可靠性建模,实现了 AADL 可靠性模型到广义随机 Petri 网可靠性计算模型的转换,
并基于 GSPN 可靠性计算模型对嵌入式系统进行可靠性评估,设计并实现了 AADL 可靠性评估工具.此
外,AADL 本身还是一种半形式化的建模语言,无法保证所建立的 CPS 模型的安全性,因此有必要对使用 AADL
建模的模型进行安全性验证.
通信顺序进程 CSP(communicating sequential process)是 Hoare [10] 在 1978 年建立的一种适合于分布式并发
软件规格和设计的形式化方法.1986 年,牛津的 Reed 和 Roscoe 对 CSP 进行了实时扩展,提出了时间通信顺序进
程 TCSP(timed communicating sequential process) [11] .进程代数是一种解决并发系统通信问题的形式化方法,能
够描述 CPS 中的事件的并发、同步、异步等问题.但是 TCSP 是离散模型,且只有时间性质的描述能力,因此有
必要对 TCSP 进行空间描述能力与连续行为能力的扩展,扩展后的 TCSP 能够对 CPS 的时空一致性进行验证.
通过以上分析,本文针对 CPS 时空不一致的安全性验证问题,提出了面向 CPS 时空性质验证的混成 AADL
建模与模型转换方法(如图 1 所示).
• 该方法首先在工业界广泛使用的建模语言 AADL 上扩展时空性质,使其具有建模 CPS 时空性质的能
力,提出了混成 AADL(hybrid AADL,简称 HAADL);
• 其次,扩展了 TCSP 的条件执行算子与条件中断算子,提出了混成位置时间通信顺序进程 HP-TCSP
(hybrid position TCSP),使其具有描述时空性质的能力;
• 再次,通过模型转换方法,将扩展后 AADL 所建立的模型转换成进程代数模型进行验证,对没有通过验
证的 HAADL 模型修改其输入/输出参数,直至通过时空一致性验证;
• 最后,通过一个飞机避撞系统的实例来说明该方法在验证 CPS 时空安全性方面的有效性.