随着社会的进步及人们日益对物质文化的需要,电梯作为一种便捷的交通工具在人们的生活中已凸显出不可或缺的作用。在不断更新的电梯系统中,要求各电梯子系统之间必须具有良好的协调性以方便人们对电梯的使用。此外,为了提高电梯系统的使用效率,使得作为电梯中枢的电梯群控系统在整个电梯系统中所占据的地位极为重要。为了从各方面提高电梯的服务效率,如何有效地采用形式化模拟及验证技术对模型进行形式化模拟及验证是亟待解决的问题之一。已有的众多解决方案都仅仅是基于某一具体功能模块设计的,极少针对整体系统进行设计。不仅如此,它们还缺少对系统有效性的形式化描述。对于大型系统的软件开发,形式化开发是保证系统的有效性及准确性的一种重要软件开发方法。从电梯系统高安全性出发,由于形式化验证的不完备性,常常辅之以数据仿真。Petri网是一种强大的适用于离散系统的数学建模工具,它不仅能够很好地刻画异步并发,还具备良好的图形表示能力,更有着严密的数学理论作为支撑。从60年代诞生至今,发展历经40余载,从其得以广泛的应用足以彰显其强大的建模及模型验证能力。本文在充分了解国内外电梯发展的概况及电梯群控技术的各种算法及优劣性后,引入Petri网这一形式化数学建模工具直观地描述离散事件系统的各种关系与行为及对电梯群控系统进行了建模分析。其次,分析了电梯的运行行为和规则,使用Petri网这一建模工具给出了电梯群控系统的有效模型。该模型除了整体设计外还包括电梯低速与高速的切换以及根据现有交通模式切换不同停留模式的实现细节,还可以根据不同的需要嵌入其它功能。最后,通过分析模型,对系统模型进行简化,利用Petri网的S-不变量及可达标识图等技术对模型的有效性及准确性进行了验证,此外,通过采用Hips仿真软件对模型的性质再次进行了分析验证。