《表3 第2次精化模型需求描述》

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

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

《井下无人驾驶机车运行过程控制的建模与验证》

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

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

本次精化模型对系统连续行为进行建模。系统中机车速度和机车位置是连续变化的，因此属于连续行为。由于Event-B不支持对连续行为进行建模，但文献[12]给出一种基于时间函数的解决方法，本文采用该方法对机车运行过程的连续行为进行建模。该精化模型需求描述见表3所列。