| 研究課題/領域番号 |
15H02687
|
|---|
| 研究機関 | 国立研究開発法人産業技術総合研究所 |
|---|
研究代表者 |
磯部 祥尚 国立研究開発法人産業技術総合研究所, 情報技術研究部門, 主任研究員 (50356458)
|
|---|
| 研究分担者 |
花井 亮 国立研究開発法人産業技術総合研究所, ロボットイノベーション研究センター, 研究員 (10521255)
大岩 寛 国立研究開発法人産業技術総合研究所, 情報技術研究部門, 研究グループ長 (20415649)
BIGGS Geoffrey 国立研究開発法人産業技術総合研究所, ロボットイノベーション研究センター, 主任研究員 (20534803)
Affeldt Reynald 国立研究開発法人産業技術総合研究所, 情報技術研究部門, 主任研究員 (40415641)
安藤 慶昭 国立研究開発法人産業技術総合研究所, ロボットイノベーション研究センター, 研究グループ長 (50371018)
中坊 嘉宏 国立研究開発法人産業技術総合研究所, ロボットイノベーション研究センター, 研究グループ長 (70360609)
|
|---|
| 研究期間 (年度) |
2015-04-01 – 2018-03-31
|
| キーワード | 協調ロボット制御 / 形式仕様記述・検証 / 定理証明器 / 並行処理 / ロボットソフトウェプラットフォーム / 有限状態マシン |
|---|
| 研究実績の概要 |
ロボット制御の形式化については、ロボットアームを主な対象として、キネマティクス（ロボットの運動学）の形式化を行なっている。具体的には、剛体変換の様々な表現（等長写像 isometries, 同次表現 homogeneous representation, Denavit-Hartenberg変換, らせん運動 screw motions）を定理証明支援系Coq上に形式化した。形式化した剛体変換によるロボットマニピュレータの形式化への適用事例として、SCARA型ロボットの振舞いをCoq上に形式化した。その成果を形式検証の国際会議（CPP2017）で発表した。
協調ロボットの設計と検証については、2台の移動ロボットが協調して荷物を搬送する動作を対象として、並行処理の形式仕様記述言語CSPによるモデル化と分析の方法を研究している。その分析方法の一環として、開発中の協調動作の可視化ツールの可読性を改善するため、遷移条件式を最簡形に変換するQuine-McCluskey法を実装し、特にデッドロックの可能性の可視化を行なった。一方、特殊な例に対しては期待通りの状態削減ができない問題を確認したため、その解決を2017年度の課題に追加した。
協調ロボットの実装については、ロボットソフトウェプラットフォームOpenRTM-aistに有限状態マシンの仕様FSM4RTCを実装しており、その枠組みにCSPの同期通信方式を実装する方法を検討した。その結果、既存のデータポートのままではCSPの通信方式の実装は難しく、CSP専用の新規のインターフェース定義が必要となることが明らかとなった。その成果を計測自動制御学会の講演会で発表した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
3: やや遅れている
理由
2016年9月に、分析モデルの機能向上において分析結果の不具合（特殊な振舞いの抽象度を上げることで、状態数をより削減出来ると考えたが、当初の想定に反し、十分に削除できない問題）を確認した。別の特殊な振舞いの例では、状態を削減できていたため発見が遅れてしまった。理論レベルで不具合の原因を検討・修正することが必要不可欠なめ、アルゴリズムの機能向上と並行して実装する作業を2017年度に延期する必要性が生じた。
|
| 今後の研究の推進方策 |
2017年度、ロボット制御の形式化にかかるコストを削減するため、その表現に必要な漸近的手法を効率よく形式化するライブラリを構築する。また、2016年度の研究過程で明らかったになった２つの問題、（1）協調ロボットの動作可視化ツールが特殊な例に対しては期待通りの状態削減をできない問題と（2）FSM4RTCへのCSP通信方式の実装が難しい問題について、協調ロボットの設計、検証、実装の一貫性を重視しつつ、その課題を整理して対応策を検討し、研究を進める。
|
