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

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

何操作.时间的单位为秒,时间按照 t=t+1 变化.上下两层灯的坐标分别为 z 轴的 z 1 ,z 2 .该感应灯系统中,包含声音
控制系统 SOCON 与感光系统 LICON 和人体感应系统 PER.
• 整个系统进程 SYSAGENT 由 SENSE,STANDBY 与 ERROR 进程组成,即:
¾ PV={SOCON,LICON,PER,SENSE,STANDBY,ERROR,SYSAGENT};
¾ DV={sv,lv,x,y,z,t,z 1 ,z 2 }.
• 进程进行通信的信道 CHANNEL={sound,light,cx,cy,cz}.
其中,
• SOCON=sound?sv→STOP;
• LICON=light?lv→STOP;
• PER=cx?x→STOP||cy?y→STOP||cz?z→STOP;
• ON=turnon→STOP;
• OFF=turnoff→STOP;
• SENSE=sound!sv→STOP||light!lv→STOP||cx!x→STOP||cy!y→STOP||cz!z→STOP;(t:=0)&&(t=t+1)&&
Place(x,y,z)&t≤120&(sv=1)&(lv=1)>>ON (t>120)AOFF;SENSE.
2
2
其中,Place(x,y,z)中的坐标需满足(x +y ≤4)&&(z−6>z 2 )&&(z+6<z 1 );
• STANDBY=sound!sv→STOP||light!lv→STOP||cx!x→STOP||cy!y→STOP||cz!z→STOP;(t:=0)&&(t=t+1)
&&Place(x,y,z)&t≤120&(sv=1)&(lv=1)>>ON (t>120)AOFF;STANDBY.
2
2
其中,Place(x,y,z)中坐标需满足(x +y ≤4)&&(z−6>z 2 )&&(z+6<z 1 );
• ERROR=call→STOP;
d d
• SYSAGENT=SOCON||LICON||PER||SENSE STANDBY ERROR(d=10s).
3 扩展后的 AADL 到 HP-TCSP 的转换规则(验证)

为了验证扩展后的混成 AADL 的时空一致性,我们采用形式化的方法进行验证.接下来,先给出 HAADL 到
HP-TCSP 模型转换框架,再定义从 HAADL 到 HP-TCSP 的映射规则.

3.1 HAADL到HP-TCSP的模型转换框架
HAADL 到 HP-TCSP 模型转换框架的核心模块为同构化、语义映射和语法转换.其中,语法转换和语义映
射都是构建在所产生的元模型的基础上.对于 HAADL 模型和 HP-TCSP 模型而言,同构化的结果是建立了相互
理解的 HAADL 元模型和 HP-TCSP 元模型.语义映射模块针对同构化所产生的 HAADL 元模型和 HP-TCSP 元
模型构造语义映射规则,通过执行该转换规则,可以将符合 HAADL 元模型的 HAADL 模型转换为符合 HP-
TCSP 元模型的 HP-TCSP 模型(反之亦然).语法转换同样是基于 HAADL 元模型和 HP-TCSP 元模型构造
HAADL 语法规则和 HP-TCSP 语法规则,通过应用该语法规则,就可以将 HAADL 模型和 HAADL 文本进行相
互转换、HP-TCSP 模型和 HP-TCSP 文本进行相互转换.值得注意的是:图 6 中的 HAADL 模型和 HP-TCSP 模
型相互转换所应用的语义映射相当于是语义映射规则的实例;而 HAADL 语法转换和 HP-TCSP 语法转换分别
为 HAADL 语法规则和 HP-TCSP 语法规则的运行实例.
3.2 混成AADL到HP-TCSP的转换规则
扩展的混成 AADL 的行为附件 ExAction:={Vars,States,Transition,Time,Position}可以对应到转换过程如下.
(1) 行为附件中的 HAADL 系统变量、时间变量、位置变量中的 Interger,Float,Boolean 和 String 的基本
类型分别直接映射到 HP-TCSP 离散变量集合中的 InterType,RealType,BooleanType 和 StringType;
(2) 将状态集合中的状态对应于 TCSP 中的一个进程;