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

陈小颖 等:面向 CPS 时空性质验证的混成 AADL 建模与模型转换方法 1795

接下来,针对图 G′进行时空一致性的算法验证(如图 9 所示).

N 0
(5,tc, dis,(x danger,y danger,z danger) )
(4,wait)
(2,wait) (2,wait)
N 1
(5,et, dis,(x in,y in,z in) )
(5,et, dis,(x in,y in,z in) )
(5,et, dis,(x in,y in,z in) )
(
N 6
N 4 N 5
(2,wait) (6,dsd, dis,(x leave,y leave,z leave) )
(5,mt, dis,(x leave,y leave,z leave) )
(8,cb, dis,(x leave,y leave,z leave) )
(2,wait) (2,wait)
(1,wait)
N 9 N 11
N 10
(5,mt, dis,(x end1,y end1,z end1) ) (8,cb, dis,(x end1,y end1,z end1) )
1 ) )
(6,dsd, dis,(x end1,y end1,z end1
N 14 N 15 N 16
(1,wait) (2,wait)
(2,wait)

Fig.9 Normal reachable graph G′
图 9 规范的可达图 G′
各个节点的限制 restrict[ ]={0,9,16,16,16,16,16,28,29,22,27,24,40,40,27,34,34},表示从源节点 N 0 到当前节
点 N i 的时间限制.该限制数组可以从以往的知识库中获取.通过时空一致性检查算法,返回值为 false,存在时间
不一致的问题,且 consist_abnormal 值为{N 10 ,N 14 },在 N 10 处的时空不一致是本应在时间 26 到达(x leave ,y leave ,z leave )
处,当前避撞飞机预计在时间 27 到达,存在时空不一致现象,此时提高 HAADL 中输入的飞机速度,以便在规定时
间 26 到达(x leave ,y leave ,z leave )处,或启用自动避撞系统进行容错处理,并输出一定的反馈信号.在 N 14 处的时空不一
致是本应 28 时间到达(x end ,y end ,z end )处,但预计飞机在时间 27 到达,此时减小 HAADL 中输入的飞机速度,或启用
自动避撞系统进行容错处理,并输出一定的反馈信号,例如协调两架飞机、指示另一架飞机加速等措施.

5 相关工作比较

CPS 系统是一个综合计算、网络和物理环境的多维复杂系统,对 CPS 的建模应该考虑系统的时空一致性.
一方面,近年来对 AADL 扩展以及利用 AADL 对 CPS 进行建模与验证,国内外已有相关研究.文献[6]针对 CPS
的连续行为以及网络组件和物理组件之间的交互进行建模,提出了构造新的 AADL 子语言 AADL+的方法.文献
[7]通过扩展 AADL 的标准和附录,实现对计算实体、物理实体和交互实体的统一描述.文献[8]将 AADL 和
Simulink/Stateflow 的结合起来,提供了统一的图形化协同建模形式,从软件、硬件和物理这 3 个角度支持 CPS
的设计.这部分工作主要侧重于研究 CPS 的计算、网络和物理环境之间的交互与融合方面.文献[15]在 AADL
行为附件上进行层次化扩展,从而使行为附件中具有表达层次自动机的机制.文献[16]等将 AADL 与 Z 结合,对
嵌入式软件可靠性进行建模与评估,并在 此基础上扩 展了概率进 行可靠性评 估 .文献[17]扩展了进程代数
CCS,提出 HPCCS 进行建模并扩展 AADL 的行为附件描述随机动作.文献[18]针对混成 AADL 在不确定环境下
的建模与分析问题,提出了面向不确定环境的混成 AADL 设计与量化分析方法,从而支持混成 AADL 的不确定
性建模以及对混成 AADL 模型的定量分析.该部分研究主要在 AADL 上进行扩展,从而进行可靠性分析,但其更
注重系统的随机性,对时空的一致性考虑较少.文献[19]基于带有时间约束的 AADL 行为模型时序验证问题,提
出了基于节点转换规则的 AADL 行为模型分解规则,从而支持实时系统对隐式时间约束和显式时间约束的验