Realization of Multi-Car Elevator Group Controller Development System Based on Formal Methods

点击翻译按钮获取中文摘要

1. We proposed a Petri net model, a state transition model, and a mathematical programming model of multi-car elevator systems, and gave their analysis methods. 2. We established a method of specifying requirements for group controllers as temporal logic expressions. 3. We formalized basic operations of group controllers as building blocks, and proposed a method to design a new group controller by combining them. 4. We developed a method to apply SPIN model checker to the state transition model. 5. We developed a hybrid method of constraint program and mixed integer program for the mathematical programming model. And combining the results of 1. to 5., we realized a system for developing multi-car elevator group controller on the basis of formal methods.