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

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

v 1 :Base_Types::float; v 2 :Base_Types :: float;
r 1 :Base_Types::float; r 2 :Base_Types::float;
ω:Base_Types::float; distance:Base_Types::float;
direction:Base_Types:String;
times
danger_wait:Base_Types::float; in_wait:Base_Types::float;
end_wait:Base_Types::float; pr:Base_Types::float;
ct:Base_Types::float; bk:Base_Types::float;
wait:Base_Types::float; compute:Base_Types::float;
position
x danger1 :Base_Types::float; x danger2 :Base_Types::float;
y danger1 :Base_Types::float; y danger2 :Base_Types::float;
z danger1 :Base_Types::float; z danger2 :Base_Types::float;
x in1 :Base_Types::float; x in2 :Base_Types::float;
y in1 :Base_Types::float; y in2 :Base_Types::float;
z in1 :Base_Types::float; z in2 :Base_Types::float;
x leave1 :Base_Types::float; x leave2 :Base_Types::float;
y leave1 :Base_Types::float; y leave2 :Base_Types::float;
z leave1 :Base_Types::float; z leave2 :Base_Types::float;
x end1 :Base_Types::float; x end2 :Base_Types::float;
y end1 :Base_Types::float; y end2 :Base_Types::float;
z end1 :Base_Types::float; z end2 :Base_Types::float;
states
s 1 :initial state;
s 2 :state;
s 3 :state;
s 4 :complete state;
error:state;
transitions
T_0:
s 1 [〈p 1 v?v 1 |p 2 v?v 2 〉〈(distance=danger_wait*(p 1 v!v 1 +p 2 v!v 2 ))∧(wait=danger_wait)∧(compute=pr)〉]→
{s 2 [{(x danger1 ,y danger1 ,z danger1 )!|(x danger2 ,y danger2 ,z danger2 )!〉}],error]}
T_1:
s 2 [〈direction?|(x in1 ,y in1 ,z in1 )!|(x in2 ,y in2 ,z in2 )!|p 1 v?v 1 |p 2 v?v 2 〉〈 (rω 1 ) = v ∧ 1 2 (r ω 2 ) = 2 v ∧(wait=in_wait)∧
2
2
2
(compute=ct)〉]→{s 3 [{〈p 1 w:=ω|p 2 w:=ω〉}],error]}
T_2:
2
s 3 [〈direction?|(x leave1 ,y leave1 ,z leave1 )!|(x leave2 ,y leave2 ,z leave2 )!|p 1 v?v 1 |p 2 v?v 2 〉〈 ( × − r 1 ω ) = 2 1 2 ∧ v ( × r 2 − ω ) = 2 v ∧
2
(wait=end_wait)∧(compute=bk)∧(ω≠0)〉]→{s 4 [{〈ω=0|(x end1 ,y end1 ,z end1 )!|(x end2 ,y end2 ,z end2 )!〉}],error]}
**};
end example.impl;
接下来,我们将 HAADL 的行为附件通过定义的转换规则转为 HP-TCSP.
其中的状态 s 1 ~s 4 ,error 对应于进程 NORMAL,ENTRY,ROTATION,EXIT,ERROR,且 AADL 行为附件中的