2017 Fiscal Year Annual Research Report
A Development Process of Control Software for Safe Cooperative Robots
| Project/Area Number |
15H02687
|
|---|
| Research Institution | National Institute of Advanced Industrial Science and Technology |
|---|
Principal Investigator |
磯部 祥尚 国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 主任研究員 (50356458)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
花井 亮 国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 研究員 (10521255)
大岩 寛 国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 研究チーム長 (20415649)
BIGGS Geoffrey 国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 主任研究員 (20534803)
Affeldt Reynald 国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 主任研究員 (40415641)
安藤 慶昭 国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 研究チーム長 (50371018)
中坊 嘉宏 国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 研究チーム長 (70360609)
|
|---|
| Project Period (FY) |
2015-04-01 – 2018-03-31
|
| Keywords | 協調ロボット制御 / 形式仕様記述・検証 / 定理証明器 / 並行処理 / ロボットソフトウェプラットフォーム / 有限状態マシン |
|---|
| Outline of Annual Research Achievements |
ロボット制御の形式化については、ロボットアームを主な対象として、キネマティクス（ロボットの運動学）を定理証明支援系Coq上に形式化した。2017年度は、ロボットアームの動き（各関節の速度と手先の速度の関係）を表現するために、2016年度までに形式化した剛体変換の様々な表現（等長写像、らせん運動等）の形式記述を用いて、ヤコビ行列を形式化した。さらに、マニピュレータの形式化への適用事例として、SCARA型ロボットアームの動きをヤコビ行列によってCoq上に形式化し、その証明スクリプト（Coqコード）をウェブサイトGitHubから公開した。また、ヤコビ行列の形式化に必要な数学（微分等）をライブラリMathComp-Analysisとして形式化し、Coq Workshop（国際学会）で発表するとともに、形式的な実数解析のための基本技術をまとめた論文が学術雑誌に採録された。
協調ロボットの設計、検証、実装については、当初の計画では、設計から実装までをシームレスにつなぐためにCSP方式（検証に適する同期通信方式）を共通仕様としたが、CSP方式の実装機能を検討中に、同期待ちするCSP方式では実行効率の点からRTM（ロボット開発環境）に適さないことが判明し、同期待ちをしないFSM4RTC方式（実装に適する非同期通信方式）を共通仕様とする計画に変更した。この計画変更にともない、FSM4RTC方式の協調ロボットの設計を簡単に記述・検証できるように、FSM4RTC準拠の検証ライブラリを汎用モデル検査ツールFDR用に作成した。このライブラリの適用事例として、協調搬送ロボットの設計を検証・修正するとともに、OpenRTM-aist（RTMの産総研実装）用に開発中のFSM4RTC準拠の実装ライブラリを用いて検証済みの設計を実装して動作を確認し、その成果を講演会ROBOMECH2018にて発表した。
|
| Research Progress Status |
平成29年度が最終年度であるため、記入しない。
|
| Strategy for Future Research Activity |
平成29年度が最終年度であるため、記入しない。
|
