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

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

证.这部分工作主要考虑时间的约束,而对位置因素考虑的较少.文献[20]中,用 AADL 对中国列车控制系统
(CTCS-3)进行行为建模与验证.其使用核心 AADL 结构对系统的结构进行建模,利用 BLESS 附件对控制系统的
离散行为进行了建模和验证,利用混合附件对列车的连续行为和网络-物理交互进行建模,并使用定理证明的方
法进行验证.该方法具有一定的针对性,主要通过定理证明的方法对列车控制系统的离散行为、连续行为和网
络-物理交互进行建模;本文方法主要是从模型检测的角度对 CPS 验证,两种方法具有一定的互补性.不同方法
研究 CPS 的侧重点各不相同,与以上工作不同,本文更加注重 CPS 的非功能属性,并且从 AADL 进行建模入手,
通过模型转换,将其转换成形式化模型进行模型检测.该方法是对已有方法的有效补充,能够在实际应用上发挥
一定的效用.
另一方面,关于 CPS 的时间或空间性质建模与验证问题,国内外已有相关研究.文献[21]提出了基于时间状
态迁移矩阵的形式化建模方法,在迁移矩阵形式语义基础上,引入时钟函数与时间约束,从而实现在软件设计层
面逻辑功能与时间性能的一体化建模与验证.文献[22]通过定义一系列的规则,将领域环境模型组合到运行时
验证过程中.该方法研究环境的变化对系统参数的实时影响,但未将系统本身的空间随着时间的变化考虑在内.
文献[23]把 CPS 系统分为物理实体、计算实体和控制实体,并给出基于动态行为建模的 UML 建模方法对 CPS
系统计算实体进行建模,从而完整地把系统计算实体的逻辑关系和时序关系描述出来.文献[24,25]在时间条件
约束下,对 CPS 系统各部分之间如何安全交互进行建模研究.这些传统的 CPS 建模与验证方法大多局限于时间
域内的分析,对于时间与空间统一变化对 CPS 的影响考虑的较少,因此可能会存在一些 CPS 时空一致的安全性
问题.
文献[26]将 CPS 时空状态转移融合成一个状态转移实时时空事件,并在时间 Petri 网基础上引入空间标签,
建立时空 Petri 网模型,利用时空 Petri 网对物理实体状态转移过程进行分析.文献[27]针对运输信息物理融合系
统(T-CPS)缺乏时空建模与分析问题,提出了有色时空 Petri 网(CSTPN),并用 CSTPN 交通路口协调控制系统的
开发、交通仿真分析以及基于 T-CPS 的 CSTPN 的实现.这部分方法更加注重于 CPS 的时空性质的建模方面,
本文是已有工作的延续工作,本文中加入了时空一致性的验证,从而能够保证 CPS 的时空安全性.
与以上研究工作相比,本文重点研究非功能属性中的时间与空间属性,即时空不一致对系统安全性的影响,
重点关注 CPS 时空一致性的建模与验证.本文方法是对已有工作的有效补充.本文首先在半形式化的 AADL 上
作时空性质的扩展;其次,在形式化 TCSP 上扩展空间属性;再次,将扩展的 HAADL 转化成扩展后的 HP-TCSP
并进行时空一致性的验证,从而保证 CPS 的时空安全性.

6 结束语

CPS 的安全性问题受到人们的广泛关注.针对验证 CPS 时空不一致的安全性问题,本文提出了面向 CPS 时
空性质验证的混成 AADL 建模与模型转换方法.首先,在 AADL 的行为附件中扩展时间与空间因素;其次,在
TCSP 中引入微分方程以及位置描述,提出了 HP-TCSP,能够验证 CPS 的时空性质;再次,通过模型转换,将
HAADL 转换为 HP-TCSP,从而可以将 HAADL 描述的 CPS 模型在 HP-TCSP 中进行时空一致性验证;最后,通过
一个飞机避撞系统实例验证该方法的有效性,从而保障 CPS 的时空安全性.
但是在转换的过程中,大多是根据转换规则进行手动转换,接下来将会完成一个自动转换系统,实现
HAADL 到 HP-TCSP 的自动转换.
本文主要研究关于 AADL 行为附件的扩展,对于 AADL 组件的物理附件的扩展并没有过多讨论,关于
AADL 物理附件的扩展模块将会在后续的研究工作中继续展开研究.
CPS 系统场景复杂,对于时间不一致的容错处理部分,我们也将继续展开研究.此外,时间与空间的变化也伴
随着空间拓扑关系的变化,如何解决物理空间与时间变化约束的 CPS 安全问题,将会是下一步的研究重点.
CPS 运行环境复杂,且在目前发展环境下应用场景较为广泛,例如自动驾驶等,这些具体复杂的场景中不仅
有整体的时空一致性,其内部也包含了一定的时空一致性.因此,如何实现时空一致性的整体与部分的组合形式
化验证,也是接下来的一个研究方面.