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

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

HAADL HP-TCSP
语法转换
语法规则 语法规则

元建模 HAADL HP-TCSP
元模型 元模型

符合 符合
语义映射 语义映射规则

符合
符合 符合
语义映射
HP-TCSP
HAADL模型
模型
HAADL HP-TCSP
语法转换 语法转换

HAADL文本 HP-TCSP文本

Fig.6 Framework of model transformation from HAADL to HP-TCSP
图 6 HAADL 到 HP-TCSP 模型转换框架
(3) 行为附件中的状态迁移映射:
Trans_sequence:=SourceState[〈act 1 〉〈guard〉]→{DesS 1 [{〈act 2 〉}],DesS 2 [{〈act 3 〉}],...,error]}.
guard 对应两种形式:周期执行 on dispatch 与条件执行.接下来,我们对 guard、act 1 、act 2 (迁移序列中
的 act 1 与 act 2 形式转换相同)、error 与迁移序列分别转换.
(3.1) guard 是变迁触发的条件,一般包括定时触发、条件触发与端口发生的输入/输出事件触发.定时
d
触发(time trigger)如 t=d 转换为 PQ ,P 为一个不会与任何进程通信的进程,则在 d 时间后执行
进程 Q;条件触发(condition trigger)对应于 HP-TCSP 中的条件执行算子 Con>>P 算子 Con 中与
P Fin_Con(Fin_Con:=Fcon|true)AQ 算子 Fcon 的条件;端口输入/输出事件触发用 HP-TCSP 中
的输入/输出事件表示;
(3.2) act 1 ,act 2 等中动作可以转换为 HP-TCSP 的条件执行算子中的微分方程变量值的变化.引入 3 个
运算符 vara?varb,vara!varb 转换为微分方程中变量的赋值变化,多个动作同时进行‘|’,每个动作
转换为只有一个事件的进程,多个动作同时进行表示成进程之间的并发;
(3.3) error 对应于 HP-TCSP 中的 ERROR 进程;
(3.4) 迁移序列即未在条件 interrupt 执行的迁移状态,会执行下一个状态.将其转换为:
P (interrupt)AQ.
其中,P 为迁移序列的前一个状态转换的进程,Q 为迁移序列的后一个状态转换的进程.
3.3 HAADL到HP-TCSP的具体映射规则
根据第 3.2 节的转换策略,我们定义了从 HAADL 到 HP-TCSP 的转换规则,见表 1.
在实现 HAADL 到 HP-TCSP 的转换后,即可得到位置时间迁移系统的状态空间图,再通过第 2.5 节的时空
属性分析的算法对其进行时空属性的检查,并对 HAADL 做相应的修改与容错.