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)
|
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.
|