当今工作与生活节奏越来越快,电梯在每一栋高楼大厦中都起着不可或缺的作用。与此同时,电梯调度的安全问题也越来越受到政府和人民的关注。电梯调度的安全问题就是在满足电梯质量安全的前提下如何调度电梯车厢的运行以尽可能地节约用户时间、节约电梯耗能。传统的电梯组调度方法的优化目标单一,并且无法检测调度方案是否存在安全隐患,不能更好地根据实际情况进行调度。而模型检测的思想是将电梯组调度的可能情况模拟成行为系统,将期望的调度结果用性质语句描述,验证系统是否符合性质语句。将模型检测的自动化思想运用在电梯组调度工作上,不仅可以很好地解决电梯组调度的问题还可以对电梯组调度方案的安全性进行检测。因此,将模型检测技术运用于电梯组调度是十分恰当的。根据电梯组的实际情况,分别针对电梯使用的三种时间段:上行高峰期、下行高峰期和层间交通期应用模型检测的技术和思想来解决目标层预约的电梯组调度问题。SPIN、UPPAAL与NuSMV是当前比较流行的三种模型检测工具,为了找到适合描述和验证电梯系统安全性质的工具,先是构建了一个简单的单电梯分布式电梯系统模型,用它们验证该模型的相关性质并进行比较。具体地,先用SPIN、UPPAAL及NuSMV对电梯系统建模,比较它们建模语言之间的特点。再分别使用三种验证工具进行多项重要性质的验证,分析这些对同一个分布式实时系统验证的效果。最后,总结了三种模型检测工具各自的特性。实验结果表明,SPIN与NuSMV更适合验证分布式系统,而UPPAAL更适合验证实时系统,SPIN更适合描述和验证预约层电梯组调度系统。基于此,本文使用模型检测工具SPIN验证由PROMELA语句构成的目标层预约电梯组模型。先验证模型有关安全性的相关性质,再将期望的调度结果设置成需要检测的LTL性质语句进行验证。如果存在较为优秀的调度方案,SPIN将会自动化生成。通过分析几个对比实验的结果,发现将SPIN运用于目标层预约电梯组调度可以取得更优化的调度结果。