Elevator Group Control System Design Based On Petri Nets

Elevators, as a class of convenient transportation means, play an indispensable role in people’s lives with the progress of the society and more material and cultural requirements. In a constantly updated elevator system, it is required that its elevator sub-systems possess well coordination properties for people to use and increases elevator service efficiency. Hence, the elevator group control system, as a control center, plays a key role in a physic elevator. In order to improve the service efficiency of an elevator, how to develop a formalized elevator model to verify its properties is one of the problems urgently waiting to be solved. The existent solutions are designed only based on a specific function module, which do not consider the design problem in an overall level. Moreover, they are lack of a formalized description to analyze the system effectiveness. Formal technologies are an important software development approach to guarantee the effectiveness and the correctness of a large software system. On the other hand, data simulation contains important means to supply incomplete formal technologies.Petri nets are a key mathematical tool to model discrete systems. They are not only depicting asynchronous and concurrent behavior, also possess visualized graphical representations and rigorous mathematical supports. Petri nets had been used widely after more than 40 years owing to their powerful modeling and model validation abilities.This thesis deals with the domestic and foreign elevator developments, the existent elevator control algorithms, and their advantages and disadvantages. Petri nets as a formalized modeling tool are applied to describe complex event relations and the behavior of discrete event systems, which are used to model elevator group control systems.Then, this thesis analyzes the running operations and the rules of an elevator. An effective elevator group control system is proposed by using Petri nets. An overall system formalized design is presented. Furthermore, this work designs the functions of elevator low and high speed switching and switching different residence patterns according to existent traffic flows.The effectiveness and correctness of the proposed elevator group control model are verified by using S-invariants and its reachable marking graph. Finally, the model properties are verified by using a simulation tool ’Hips’.