基于模型检测方法的目标层预约电梯组调度策略
| 摘要 | 第7-8页 |
| abstract | 第8-9页 |
| 第1章 绪论 | 第10-14页 |
| 1.1 选题背景及研究意义 | 第10-11页 |
| 1.2 论文研究内容 | 第11-13页 |
| 1.3 论文组织结构 | 第13-14页 |
| 第2章 模型检测与电梯组调度概述 | 第14-20页 |
| 2.1 模型检测工具简介 | 第14-16页 |
| 2.2 模型检测工具的研究现状 | 第16-17页 |
| 2.3 电梯调度方法概述 | 第17-18页 |
| 2.4 本章小结 | 第18-20页 |
| 第3章 单电梯单任务电梯系统验证 | 第20-42页 |
| 3.1 问题定义 | 第20页 |
| 3.2 单电梯系统模型构建 | 第20-32页 |
| 3.2.1 分布式实时单电梯系统模型 | 第20-22页 |
| 3.2.2 基于SPIN的单电梯模型 | 第22-25页 |
| 3.2.3 基于UPPAAL的单电梯模型 | 第25-29页 |
| 3.2.4 基于NuSMV的单电梯模型 | 第29-32页 |
| 3.3 性质验证及比较分析 | 第32-40页 |
| 3.3.1 SPIN验证结果与分析 | 第32-34页 |
| 3.3.2 UPPAAL验证结果与分析 | 第34-36页 |
| 3.3.3 NuSMV验证结果与分析 | 第36-39页 |
| 3.3.4 性质验证综合比较与分析 | 第39-40页 |
| 3.4 三种验证工具的适用性对比分析 | 第40页 |
| 3.5 本章小结 | 第40-42页 |
| 第4章 预约层电梯组系统验证及调度 | 第42-64页 |
| 4.1 问题定义 | 第42页 |
| 4.2 电梯调度优化的目标函数 | 第42-45页 |
| 4.3 基于SPIN的电梯调度模型 | 第45-54页 |
| 4.3.1 电梯调度规则 | 第45页 |
| 4.3.2 单电梯多任务SPIN调度模型 | 第45-48页 |
| 4.3.3 预约层电梯组SPIN调度模型 | 第48-54页 |
| 4.4 系统安全的性质验证 | 第54-59页 |
| 4.5 优化调度方案的系统性质验证 | 第59-60页 |
| 4.5.1 上行高峰期性质验证 | 第59页 |
| 4.5.2 下行高峰期性质验证 | 第59-60页 |
| 4.5.3 层间交通期性质验证 | 第60页 |
| 4.6 调度结果及分析讨论 | 第60-63页 |
| 4.6.1 上行高峰期 | 第60-61页 |
| 4.6.2 下行高峰期 | 第61-62页 |
| 4.6.3 层间交通期 | 第62-63页 |
| 4.7 本章小结 | 第63-64页 |
| 第5章 总结与下一步研究 | 第64-66页 |
| 5.1 总结 | 第64-65页 |
| 5.2 下一步研究 | 第65-66页 |
| 参考文献 | 第66-70页 |
| 攻读硕士学位期间研究成果 | 第70-71页 |
| 致谢 | 第71-72页 |
