《表3 CAL＿EOA及其验证模型的问题图的交互列表》

  提示：宽带有限、当前游客访问压缩模式

本系列图表出处文件名：随高清版一同展现

《区域控制器的安全需求建模与自动验证》

1. 获取 高清版本忘记账户？点击这里登录

1. 下载图表忘记账户？点击这里登录

从上述描述中，我们可以得到交互集合IS，IS={int1，int2，…，int48}，其中，{int1，…，int9}为Train发送给CAL＿EOA的列车定位信息，{int10，int11}为CAL＿EOA发送给列车的EOA报文，{int12，…，int15}为Block发送给CAL＿EOA的BLOCK逻辑分布，{int16，…，int18}为Branch发送给CAL＿EOA的Branch逻辑分布，{int19，…，int22}为Block Layout发送给CAL＿EOA的Block实体分布，{int23，…，int25}为Branch Layout发送给CAL＿EOA的Branch实体分布，{int26，…，int34}为Other Train发送给CAL＿EOA的其他列车定位信息，{int35，…，int37}为Signal发送给CAL＿EOA的信号机位置和状态，{int38，int39}为ZC boundary发送给CAL＿EOA的区域控制器边界信息，{int40，…，int42}为Traffic Direction发送给CAL＿EOA的Block的可行驶方向信息，{int43，…，int45}为Buffer Zone发送给CAL＿EOA的SI后的缓冲区信息，{int46，int47}为Overlap发送给CAL＿EOA的重叠区信息，int48为Train发送给CAL＿EOA的报文接受状态.上述交互inti（1≤i≤48）的定义及变量的含义具体见表3.