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

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

( ω
2
2
in_wait)&(compute=ct)>>ROTATION (( ω r 1 ) ≠ v 1 2 ∨ r 2 ) ≠ v ∨wait≠in_wait∨compute≠ct)AERROR;
2
2
• ROTATION=direction?→STOP||(x leave1 ,y leave1 ,z leave1 )!→STOP||(x leave2 ,y leave2 ,z leave2 )!→STOP||p 1 v?v 1 →
2
2
STOP||p 2 v?v 2 →STOP||p 1 w?→STOP||p 2 w?→STOP|| (( ×−r 1 ω ) = v 1 2 ) & &(( × −r 2 ω ) = v 2 2 ) &&(wait=end_wait)
2
&(compute=bk)&ω≠0>>EXIT (( × − r ω ) ≠ 2 2 ∨ v ( × r − ω ) ≠ 2 v ∨wait≠end_wait∨compute≠bk)AERROR;
1 1 2 2
• EXIT=(ω=0→STOP||(x end1 ,y end1 ,z end1 )!→STOP||(x end2 ,y end2 ,z end2 )!→STOP)>>EXIT (ω≠0)AERROR;
• ERROR 定义为一系列容错措施.
HP-TCSP 的状态空间对应于一个位置时间迁移系统,针对于不同的指令,其所需的等待时间与执行时间不
同.表 4 展示了事件等待时间与执行时间.
Table 4 Time for aircraft collision avoidance
表 4 飞机避撞的时间
事件 等待时间 执行时间 所处位置(p 1 飞机/p 2 飞机)
进入轨道(et) 2 5 (x danger1,y danger1,z danger1)/(x danger2,y danger2,z danger2)
左转(lf) 3 8 (x in1,y in1,z in1)/(x in2,y in2,z in2)
右转(rt) 3 8 (x in1,y in1,z in1)/(x in2,y in2,z in2)
爬升(cb) 2 8 (x in1,y in1,z in1)/(x in2,y in2,z in2)
下降(dsd) 2 6 (x in1,y in1,z in1)/(x in2,y in2,z in2)
平飞(mt) 1 5 (x in1,y in1,z in1)/(x in2,y in2,z in2)
离开(lf/rt/cb/dsd/mt 与以上避撞时的方向相反) 3 8 (x leave1,y leave1,z leave1)/(x end2,y end2,z end2)

其状态空间图 G 如图 8 所示:首先,先通过算法 1 获取一个规范的可达图,若本次最坏执行时间 worst_
execute 为 36.我们对比每一条路径的执行时间.通过最坏时间可满足性算法,得到返回值为 false,获取异常节点
集合 abnormal={N 12 ,N 13 }.由于{N 0 N 1 N 2 N 7 N 12 }与{N 0 N 1 N 3 N 8 N 13 }的执行时间 totalt 值为 38,则该两条路径的总执
行时间不满足最坏执行时间的要求,说明在当前状态下,采取左转右转方式避撞会有碰撞危险,因此删除仅属于
这两条路径的节点与迁移边,然后得到状态空间图 G′.此外,修改 HAADL 中的 direction 的输入为爬升、下降或
平飞.

N 0
(5,tc, dis,(x danger,y danger,z danger) )
(4,wait)
(2,wait) (2,wait)
(2,wait) N 1
(2,wait)
(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) )
(5,et, dis,(x in,y in,z in) ) (5,et, dis,(x in,y in,z in) ) (
(2,wait)
N 2 N 3 N 4 N 5 N 6
(8,rt, dis,(x leave,y leave,z leave) )
(5,mt, dis,(x leave,y leave,z leave) ) (6,dsd, dis,(x leave,y leave,z leave) )
(8,if, dis,(x leave,y leave,z leave) ) (8,cb, dis,(x leave,y leave,z leave) )
(3,wait) (3,wait) (1,wait) (2,wait) (2,wait)
N 7 N 8 N 9 N 10 N 11
(5,mt, dis,(x end1,y end1,z end1) ) (8,cb, dis,(x end1,y end1,z end1) )
(8,rt, dis,(x end1,y end1,z end1) )
1 )
(8,if, dis,(x end1,y end1,z end1) ) (6,dsd, dis,(x end1,y end1,z end1) )
N 12 N 13 N 14 (1,wait) N 15 N 16
(3,wait) (3,wait) (2,wait) (2,wait)

Fig.8 Position-time transition system G of aircraft collision avoidance
图 8 飞机避撞的位置-时间迁移系统 G