| 研究課題/領域番号 |
15H02687
|
|---|
| 研究機関 | 国立研究開発法人産業技術総合研究所 |
|---|
研究代表者 |
磯部 祥尚 国立研究開発法人産業技術総合研究所, 情報技術研究部門, 研究グループ付 (50356458)
|
|---|
| 研究分担者 |
花井 亮 国立研究開発法人産業技術総合研究所, ロボットイノベーション研究センター, 研究員 (10521255)
大岩 寛 国立研究開発法人産業技術総合研究所, 情報技術研究部門, 研究グループ長 (20415649)
BIGGS Geoffrey 国立研究開発法人産業技術総合研究所, ロボットイノベーション研究センター, 主任研究員 (20534803)
Affeldt Reynald 国立研究開発法人産業技術総合研究所, 情報技術研究部門, 主任研究員 (40415641)
安藤 慶昭 国立研究開発法人産業技術総合研究所, ロボットイノベーション研究センター, 研究チーム長 (50371018)
中坊 嘉宏 国立研究開発法人産業技術総合研究所, ロボットイノベーション研究センター, 研究チーム長 (70360609)
|
|---|
| 研究期間 (年度) |
2015-04-01 – 2018-03-31
|
| キーワード | 仕様記述・検証 / 協調ロボット制御 / 定理証明器 / 並行処理解析器 / ロボットソフトウェプラットフォーム |
|---|
| 研究実績の概要 |
協調ロボットの設計と検証については、2台の移動ロボットが協調して荷物を運搬する動作を形式仕様記述言語CSPでモデル化し、その協調動作を分析した。この移動ロボットのモデルは離散状態と連続値をもつ状態遷移系である。このモデルに対して、開発中のCONPASUツールを適用し、連続値をもつ複数の状態遷移系を並行合成して、協調動作を可視化できることを確認した。また、CSPによる他の検証例として、セキュリティプロトコルの検証も行い、電子情報通信学会大会にて発表した。これらの事例をもとに、2016年度は、より可読性の高い可視化方法の検討と、CONPASUツールの改善を行う。
ロボット制御の形式化については、キネマティクス（ロボットの運動学）の基礎となる性質を定理証明器Coq上に形式化した。この形式化を行うため、11月16～25日にフランスの国立情報学自動制御研究所（INRIA）の Cyril Cohen博士を招へいした。Cohen博士はCoqの代数ライブラリの開発者である。Cohen 博士の代数ライブラリを用いて、キネマティクスの基礎となる座標、回転、剛体力学の基本的性質を、定理ライブラリ（2,385行）としてCoq上に形式化した。この成果をもとに、日本ソフトウェア科学会からの依頼で原稿「Mathematical Components の入門」を執筆した（2016年度中に掲載予定）。2016年度はキネマティクスの形式化を継続するとともに、ロボットアームの座標系の形式化方法も検討する。
CSPの同期型メッセージパッシング通信方式を、ロボットソフトウェプラットフォームOpenRTM-aistに導入するため、RTミドルウェアのOMGの標準規格との整合性を検査し、その実現方法を検討した。2016年度は、OpenRTM-aistにCSP通信方式を実現するための設計を行い、実装に着手する。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
3: やや遅れている
理由
2015年4月に研究代表者（磯部）が管理部門の研究戦略部（情報技術研究部門兼務）に異動になったため、予定よりも研究時間を確保できなかった。
|
| 今後の研究の推進方策 |
2015年度に作成した協調する複数のロボット制御の並行処理モデルの例をもとに、複数のロボットを安全に制御する協調ソフトウェアの開発に必要な設計、検証、実装の技術課題を整理し、課題解決に向けて研究を推進する。具体的には、協調動作の可視化ツールのデータ解析機能の改善、定理証明器によるロボット制御座標系の形式化、協調ロボットの通信基盤の開発等を行う。また、テクニカルスタッフを雇用して、ツール開発を加速させる（現在、公募手続き中）。
|
