《表2 联锁表可能出错情况》

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

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

《矿井机车运输信号系统的Event-B建模与验证研究》

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

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

联锁表可能出错情况见表2所列，针对表2中每一项可能出现的错误，本文在被验证的联锁表中逐个加入单个错误情况，直至向联锁表中同时加入多个错误，观看Rodin平台是否能够提供出相应的错误信息。例如删除进路编号2“区段空闲检查”中的2LQ，颠倒进路编号3“区段空闲检查”中的3Q和DWQ顺序，向进路编号4中的“区段空闲检查”加入一个不相关的区段1LQ。把进路编号1“信号机”中的显示L改成U，把进路编号5“信号机”中的显示L改成LS。向进路编号6中的“联锁道岔”加入一个不相关的道岔5，删除一个原有的道岔1/2，并且把3/4的反位改成定位。把进路编号7中的“区段占用”5J/（2-5）DQ改成5J/DWQ，“区段出清”5J/DWQ改成5J/（2-5）DQ。删除进路编号7中的“敌对进路”中的6。