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
|
| Project Status |
Completed (Fiscal Year 2013)
|
| Budget Amount *help |
¥5,200,000 (Direct Cost: ¥4,000,000、Indirect Cost: ¥1,200,000)
Fiscal Year 2013: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2012: ¥1,820,000 (Direct Cost: ¥1,400,000、Indirect Cost: ¥420,000)
Fiscal Year 2011: ¥1,950,000 (Direct Cost: ¥1,500,000、Indirect Cost: ¥450,000)
|
|---|
| 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.
|
Report
(4 results)
Research Products
(40 results)
