安全な協調ロボット制御ソフトウェア開発方法の研究

2017 年度 実績報告書

• 研究課題/領域番号: 15H02687
• 研究機関: 国立研究開発法人産業技術総合研究所
• 研究代表者: 磯部 祥尚 国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 主任研究員 (50356458)
• 研究分担者: 花井 亮 国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 研究員 (10521255) ; 大岩 寛 国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 研究チーム長 (20415649) ; BIGGS Geoffrey 国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 主任研究員 (20534803) ; Affeldt Reynald 国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 主任研究員 (40415641) ; 安藤 慶昭 国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 研究チーム長 (50371018) ; 中坊 嘉宏 国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 研究チーム長 (70360609)
• 研究期間 (年度): 2015-04-01 – 2018-03-31
• キーワード: 協調ロボット制御 / 形式仕様記述・検証 / 定理証明器 / 並行処理 / ロボットソフトウェプラットフォーム / 有限状態マシン

研究実績の概要

ロボット制御の形式化については、ロボットアームを主な対象として、キネマティクス（ロボットの運動学）を定理証明支援系Coq上に形式化した。2017年度は、ロボットアームの動き（各関節の速度と手先の速度の関係）を表現するために、2016年度までに形式化した剛体変換の様々な表現（等長写像、らせん運動等）の形式記述を用いて、ヤコビ行列を形式化した。さらに、マニピュレータの形式化への適用事例として、SCARA型ロボットアームの動きをヤコビ行列によってCoq上に形式化し、その証明スクリプト（Coqコード）をウェブサイトGitHubから公開した。また、ヤコビ行列の形式化に必要な数学（微分等）をライブラリMathComp-Analysisとして形式化し、Coq Workshop（国際学会）で発表するとともに、形式的な実数解析のための基本技術をまとめた論文が学術雑誌に採録された。
協調ロボットの設計、検証、実装については、当初の計画では、設計から実装までをシームレスにつなぐためにCSP方式（検証に適する同期通信方式）を共通仕様としたが、CSP方式の実装機能を検討中に、同期待ちするCSP方式では実行効率の点からRTM（ロボット開発環境）に適さないことが判明し、同期待ちをしないFSM4RTC方式（実装に適する非同期通信方式）を共通仕様とする計画に変更した。この計画変更にともない、FSM4RTC方式の協調ロボットの設計を簡単に記述・検証できるように、FSM4RTC準拠の検証ライブラリを汎用モデル検査ツールFDR用に作成した。このライブラリの適用事例として、協調搬送ロボットの設計を検証・修正するとともに、OpenRTM-aist（RTMの産総研実装）用に開発中のFSM4RTC準拠の実装ライブラリを用いて検証済みの設計を実装して動作を確認し、その成果を講演会ROBOMECH2018にて発表した。

現在までの達成度 (段落)

平成29年度が最終年度であるため、記入しない。

今後の研究の推進方策

平成29年度が最終年度であるため、記入しない。

研究成果

• [国際共同研究] INRIA Sophia Antipolis(フランス)
  • 国名: フランス
  • 外国機関名: INRIA Sophia Antipolis
• [雑誌論文] Formalization Techniques for Asymptotic Reasoning in Classical Analysis (2018)
  • 著者名/発表者名: Reynald Affeldt, Cyril Cohen, and Damien Rouhling
  • 雑誌名: Journal of Formalized Reasoning 巻: 11 ページ: 43-76
  • DOI: 10.6092/issn.1972-5787/8124
  • 査読あり / オープンアクセス / 国際共著
• [学会発表] 協調ロボット制御ロジックの設計モデル検証 (2018)
  • 著者名/発表者名: 磯部 祥尚
  • 学会等名: 第21回CSP研究会
• [学会発表] 協調ロボット制御ロジックの形式的なモデル化と検証 - FSM4RTC のための有限状態マシン設計の信頼性向上 - (2018)
  • 著者名/発表者名: 磯部 祥尚, 安藤 慶昭, 宮本 信彦, Biggs Geoffrey, 大岩 寛
  • 学会等名: ロボティクス・メカトロニクス講演会 ROBOMECH2018
• [学会発表] Classical analysis with Coq (2018)
  • 著者名/発表者名: Reynald Affeldt, Cyril Cohen, Assia Mahboubi, Damien Rouhling, and Pierre-Yves Strub
  • 学会等名: The Coq Workshop 2018
  • 国際学会
• [学会発表] FSMコンポーネント実装フレームワークの提案 - FSM4RTC標準に準拠した状態遷移型コンポーネント実装 - (2017)
  • 著者名/発表者名: 安藤 慶昭, 宮本 信彦, 高橋 三郎, ビグズ ジェフ, 花井 亮, 原 功
  • 学会等名: ロボティクス・メカトロニクス講演会 ROBOMECH2017
• [備考] Formal Foundations of 3D Geometry to ...
  • URL: https://staff.aist.go.jp/reynald.affeldt/robot/
• [備考] Formal Foundations for Modeling Robot Manipulators
  • URL: https://github.com/affeldt-aist/coq-robot
• [備考] 協調ロボット制御ロジックの形式的なモデル化と検証
  • URL: https://staff.aist.go.jp/y-isobe/coop-robo/