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

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

点.该算法的输入为规范的可达图 G′.restrict[i]用来表示从源点 N 0 到终点 N i 的限制时间,通过对比每个节点的
限制时间与当前 N 0 到终点 N i 执行时间,对比目标位置与当前位置间的关系来检查其时空一致性,即,在指定的
时间里是否到达了期望位置.当算法的返回值为 true 时,说明图 G′满足时空一致性;当返回值为 false 时,说明有
时空不一致的异常点.我们获取异常点所在的位置并修改 HAADL 的输入/输出值来对 HAADL 进行一定的容错
处理.

算法 2. 时空一致性检查算法.
consist_abnormal:=∅; cur_path:={N 0};
restrict[i]; //从源点 N 0 到终点 N i 的限制时间
current:=0 //从源点 N 0 到当前的时间
repeat
N b:=last node in cur_path; //取当前路径的最后一个节点

if successor nodes of last node have been visited //删除已经访问的节点
then delete last node of cur_path;
current:=current-curr_t; //删除最后一个节点时 current 减去相关的边

else
begin
N k:=take a unvisited successor node of N b; //取一个 N b 未被访问的孩子节点 N k

current:=current+curr_t //将当前路径与该孩子节点迁移边的时间加入 current
consist:=true;
if current>restrict[k] then consist:=false; //从源节点 N 0 到当前节点 N k 的时间超过该节点时间限制
if consist=false
then consist_abnormal:=consist_abnormal∪{N k}; //如果 consist 值为 false,将异常节点记下来
else
cur_path:=cur_path∪{N k};
end
until cur_path=∅;
if consist_abnormal=∅ then
return true;
else return false;
Fig.4 Algorithm for checking space and time consistency
图 4 时空一致性检查算法
2.6 感应灯实例
下面通过一个感应灯控制系统来使用 HP-TCSP 建模,以说明 HP-TCSP 的描述能力.
感应灯控制器控制感应灯是否点亮.由两个变量控制,分别为是否有声音与是否光线较弱,即:只有当光线
弱并且有人经过发出声音时,感应灯才点亮(ON).以感应灯的垂直方向为 z 坐标,当人走到以 z 轴为中心半径为
2m的范围内,如图 5 所示,当人走在圆柱形范围内,则会触发该位置的上下两个楼层(设每层楼层之间为 6m)的感
应灯设置.点亮后,当持续时间超过 2 分钟会自动熄灭(OFF).如果感应灯在 10s 内没有亮,则启用备用灯.备用灯
的执行过程与非备用灯相同,不同的是:非备用灯在 10s 内没有点亮,则报告错误 error.
z

z 1 6
2
y

z 2 -6
x
Fig.5 Example of induction lamp
图 5 感应灯实例
设置声音变量为 sv,光亮变量为 lv.当 sv=1 时,即有声音;lv=1 时,即为黑暗.相反的,sv=0 即为无声,lv=0 即为
光亮.只有 sv=1&&lv=1 时,感应灯会亮.其余 sv=1&&lv=0,sv=0&&lv=1,sv=0&&lv=0,感应灯不会亮,即不执行任