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

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

应,因此Σ T ⊆Σ (T,C,P) .当 p n =ε∧c n =true 时,Σ T =Σ (T,C,P) ,是 P HP-TCSP 到 P TCSP 的精化关系.
那么,由定理 1 得,HP-TCSP 上所有与功能性质相关的模型检测都可以通过 TCSP 的模型检测工具完成.针
对扩展的时空性质的一致性,需要进行时空一致性分析来判断是否满足时空一致性.在产生时空不一致时,进行
一定的容错措施的处理.
2.5 时空属性的分析

HP-TCSP 的位置时间迁移系统是在 TCSP 的时间迁移系统上扩展位置因素而得到的,其状态空间可构造一
个可达图 G.G:=(NODES,EDGES,TIMES,POSITIONS)其中,
• NODES={N i |N i 为进程执行的节点,0≤i≤n};
• EDGES={e(i,j)|表示从 N i 到 N j 的一条有向边,0≤i≤n,0≤j≤n,且 i≠j};
• TIMES={t(i,j)|表示从 N i 到 N j 边 e(i,j)上的时间,若从 N i 到 N j 没有边,则 t(i,j)=∞,0≤i≤n,0≤j≤n,且 i≠j};
• POSITIONS={〈dis(i,j),p(j)〉|〈dis(i,j),p(j)〉中包含两个元素,dis(i,j)表示边 e(i,j)从 N i 到 N j 经过的距离,若从
N i 到 N j 没有边,则 dis(i,j)=∞,0≤i≤n,0≤j≤n,且 i≠j.p(j)=(x i ,y i ,z i )表示在节点 N j 时所处的位置,其中,
x i ,y i ,z i 为位置的三维坐标}.
对时空一致性的检验需要检查两个方面.一是行为模型端口分配时给出的最坏执行时间(worst-case
execution time,简称 WCET)是否满足,以保证行为附件可以在期望的时间内完成任务;二是针对时空不一致问
题的验证,即:在 t 时间本应该在 B 位置,而经过验证发现在 t 时间还处于 A 位置,此时的时空不一致问题将会产
生严重的后果.
对于第 1 个问题,本文针对状态空间图 G,首先判断 G 是否为规范的可达图,即,所有的状态空间的路径是否
都可以在 WCET 时间内完成.本文通过一个深度优先的最坏时间可满足性检查算法判断 G 是否为规范的可达
图.设定 max 的值为最坏执行时间,算法中设置 cur_path 存储当前已访问路径,abnormal 存储异常节点(即从 N 0
到当前节点的迁移总时间不满足 WCET).该算法的输入是图 G,输出为图 G 是否为规范可达图:若是规范可达图,
则该算法返回值为 true;否则,返回值为 false.最坏时间可满足性检查算法如图 3 所示.

算法 1. 最坏时间可满足性检查算法.
max:=WCET; abnormal:=∅; cur_path:={N 0}; totalt:=0;
repeat
ln:=last node in cur_path; //取当前路径的最后一个节点

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

bn:=take a unvisited successor node of ln; //取一个未被访问 ln 的孩子节点 bn

totalt:=totalt+curr_t //将当前路径与该孩子节点迁移边的时间加入 totalt
result:=true;

if totalt>max then result:=false; //从源节点到当前节点 bn 之间的执行时间值大于最坏时间 max 时 result 值为 false
if result=false
then abnormal:=abnormal∪{bn}; //如果 result 值为 false,将异常节点记下来
else
cur_path:=cur_path∪{bn};
end
until cur_path=∅;
if abnormal=∅ then
return true;
else return false;
Fig.3 Algorithm for checking the worst-time satisfyability
图 3 最坏时间可满足性检查算法
通过算法 1,当返回值为 false 时,说明图 G 并不是一个规范的可达图,图中存在执行总时间大于 totalt 的路
径,此时删除仅属于 abnormal 节点所在路径的节点与边,从而可以获得一个规范的可达图 G′.接下来对规范可
达图 G′的时空一致性进行检验(如图 4 所示).consist_abnormal 用来存放执行路径中产生时空不一致的异常节