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

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

的飞行速度分别为 v 1 与 v 2 .假设飞机在 t 时刻于某点 k 相撞,则 x 1 +t×v 1 =x 2 +t×v 2 .在存在碰撞危险的距离处,飞机
可采取垂直解脱(爬升或下降)或水平解脱(左飞或右飞)进行避撞.

Fig.7 Aircraft anticollision
图 7 飞机避撞图
图 7 中两飞机避撞过程具体场景如下.
(1) 两架飞机正常航行,即将到达危险距离;
(2) 到达危险距离 distance 时,p 1 飞机位置为(x danger1 ,y danger1 ,z danger1 )与 p 2 飞机位置为(x danger2 ,y danger2 ,z danger2 ).
在响应时间 danger_wait 时需要做出反应,即:在相距距离 distance=x 2 −x 1 =danger_wait×(v 1 +v 2 )时,飞机
要采取避撞措施.避撞措施为指定一定的方向爬升/下降/左/右/平飞.旋转飞机以碰撞中心为圆心,分
别在以 r 1 与 r 2 的半径同心圆上,以ω的角度调节方向,平滑进入各自的避撞轨道,进入点为(x in1 ,y in1 ,z in1 )
与(x in2 ,y in2 ,z in2 ),且从处于危险距离处到到达避撞轨道需 prepare(pr)时间完成,否则将启用自动避撞系
统或容错措施;
(3) 两飞机以相同大小的角速度ω在同心圆上旋转飞行,且该过程中,线速度(角速度与半径的乘积)的大
小与原飞机的运行速度大小相同,即 (rω ) = v ∧ 2 (r ω ) = 2 v ,且从到达避撞轨道到离开避撞轨道时间
2
2
1 1 2 2
需为 complete(ct),在等待时间 in_wait 时需要做出反应,否则启用自动避撞系统或容错措施;
(4) 旋转飞行结束后,两飞机以−ω的角速度在点(x leave1 ,y leave1 ,z leave1 )与(x leave2 ,y leave2 ,z leave2 )处离开避撞轨道,
在点(x end1 ,y end1 ,z end1 )与(x end2 ,y end2 ,z end2 )处到达原航行轨道,此时角速度ω为 0.该驶出避撞轨道到达正常
轨道执行时间为 back(bk),在等待时间 end_wait 时需要做出反应,否则将启用自动避撞系统或者容错
措施;
(5) 恢复正常航行.
整个过程的最坏执行时间为 worst_execute,即:该避障的过程必须在 worst_execute 前完成,以保证飞机的安
全性.该过程的 4 个关键处:到达危险距离、开始进入避撞轨道、开始离开避撞轨道、结束离开避撞轨道正常
航行.
接下来,我们用扩展的 AADL 的行为附件描述该避撞过程.
thread implementation example.impl
annex behavior_specification{**
variables