| 研究概要 |
マルチカーエレベータシステムの群管理制御器を形式手法に基づいて開発するシステムを実現するため、１．マルチカーエレベータ群管理システムのモデルの確立、２．群管理制御器の形式的な仕様記述法の確立、３．群管理制御器の系統的な構築法の洗練、４．群管理制御器のモデル検査法の洗練、５．群管理制御器の性能評価法の洗練、６．開発システムの実現を行った。
成果の概要：１．の成果：マルチカーエレベータ群管理システムに対するペトリネットモデル、S-ringを拡張した状態遷移モデル、数理計画モデルなど複数のモデルを開発し、それらの特性を明らかにした。ペトリネットモデルについては諸性質を解析する技法も明らかにした。２．の成果：時相論理による記述法を確立し、具体的な記述例のリストを作成した。３．の成果：群管理制御器の基本動作を状態遷移で形式化し、それらを組み合わせて新たな動作を構築する方法を開発した。４．の成果：状態遷移モデルに対し、モデル検査ツールSPINを適用する方法を開発した。５．の成果：数理計画モデルに対し、制約プログラミングと混合整数計画問題のハイブリッド解法を開発した。６．の成果：１～５の成果を組み合わせたマルチカーエレベータシステムの群管理制御器を形式手法に基づいて開発するシステムを実現した。
研究成果を発信するため、IEEE GCCE 2013（2013/10/1～4, 幕張メッセ）及び電子情報通信学会システム数理と応用研究会（2014/3/6～7, 愛媛大学）において、報告者らがオーガナイザとしてスペシャルセッションを開催した。さらに、システムやモデルデータは『http://web.cc.yamaguchi-u.ac.jp/~shingo/mce/』において公開している。さらに報告済みの学会誌論文及び学会発表に加え、２編の学会誌論文を投稿中である。
|
