2013 Fiscal Year Final Research Report
Realization of Multi-Car Elevator Group Controller Development System Based on Formal Methods
| Project/Area Number |
23560532
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Research Field |
Control engineering
|
|---|
| Research Institution | Yamaguchi University |
|---|
Principal Investigator |
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
MIYAMOTO Toshiyuki 大阪大学, 大学院工学研究科, 准教授 (00294041)
|
|---|
| Project Period (FY) |
2011 – 2013
|
| Keywords | エレベータ / 形式手法 / モデル化 / ペトリネット / モデル検査 / 数理計画問題 / 群管理 / 制御工学 |
|---|
| Research Abstract |
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.
|
