• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

A Development Process of Control Software for Safe Cooperative Robots

Research Project

Project/Area Number 15H02687
Research Category

Grant-in-Aid for Scientific Research (B)

Allocation TypeSingle-year Grants
Section一般
Research Field Software
Research InstitutionNational Institute of Advanced Industrial Science and Technology

Principal Investigator

Isobe Yoshinao  国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 主任研究員 (50356458)

Co-Investigator(Kenkyū-buntansha) 花井 亮  国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 研究員 (10521255)
大岩 寛  国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 研究チーム長 (20415649)
BIGGS Geoffrey  国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 主任研究員 (20534803)
Affeldt Reynald  国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 主任研究員 (40415641)
安藤 慶昭  国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 研究チーム長 (50371018)
中坊 嘉宏  国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 研究チーム長 (70360609)
Project Period (FY) 2015-04-01 – 2018-03-31
Project Status Completed (Fiscal Year 2018)
Budget Amount *help
¥16,770,000 (Direct Cost: ¥12,900,000、Indirect Cost: ¥3,870,000)
Fiscal Year 2017: ¥5,330,000 (Direct Cost: ¥4,100,000、Indirect Cost: ¥1,230,000)
Fiscal Year 2016: ¥5,850,000 (Direct Cost: ¥4,500,000、Indirect Cost: ¥1,350,000)
Fiscal Year 2015: ¥5,590,000 (Direct Cost: ¥4,300,000、Indirect Cost: ¥1,290,000)
Keywords協調ロボット / 制御ソフトウェア / 安全性 / 形式手法 / 検証 / モデル検査 / 定理証明 / 有限状態機械 / 協調ロボット制御 / 形式仕様記述・検証 / 定理証明器 / 並行処理 / ロボットソフトウェプラットフォーム / 有限状態マシン / 仕様記述・検証 / 並行処理解析器
Outline of Final Research Achievements

In order to improve the safeness of autonomous distributed cooperative robots, we applied formal methods for logically describing and verifying their control software in this research. The research result consists of the formal verification techniques for motion control by a theorem prover and for cooperative control by a model checker. For the verification of motion control, we developed a formal library about robot motion (kinematics) in the theorem prover Coq, and demonstrated its usefulness by formalizing and verifying the SCARA robot manipulator. For the verification of cooperative control, we showed how to detect design errors before the implementation by seamlessly connecting design (as finite state machines), formalization (in the specification and description language CSP), verification (by the model checker FDR), and implementation (by the middleware RTM) phases.

Academic Significance and Societal Importance of the Research Achievements

大規模IoT化が進むなか、大量のモノが高速で連携する自律・分散・協調システムの重要性が高まりつつある。その一方で、協調動作では発生確率の低いタイミング依存の不具合が潜在化する可能性があり、実装後のテストでは検出しきれないなどの問題がある。本研究では、運動制御と協調制御の形式記述と検証の作業コスト削減可能なライブラリを作成し、ロボットアームと協調搬送ロボットを例として、形式化の効果を示した。産業界への形式手法導入は容易ではないが、本研究のように、その効果と作業コスト削減の可能性を示すことによって、形式手法は今後の自律・分散・協調システムの安全性向上に資する技術となりうる。

Report

(4 results)
  • 2018 Final Research Report ( PDF )
  • 2017 Annual Research Report
  • 2016 Annual Research Report
  • 2015 Annual Research Report
  • Research Products

    (18 results)

All 2018 2017 2016 2015 Other

All Int'l Joint Research (2 results) Journal Article (2 results) (of which Int'l Joint Research: 1 results,  Peer Reviewed: 2 results,  Open Access: 2 results) Presentation (9 results) (of which Int'l Joint Research: 2 results) Remarks (5 results)

  • [Int'l Joint Research] INRIA Sophia Antipolis(フランス)

    • Related Report
      2017 Annual Research Report
  • [Int'l Joint Research] INRIA Sophia Antipolis(France)

    • Related Report
      2016 Annual Research Report
  • [Journal Article] Formalization Techniques for Asymptotic Reasoning in Classical Analysis2018

    • Author(s)
      Reynald Affeldt, Cyril Cohen, and Damien Rouhling
    • Journal Title

      Journal of Formalized Reasoning

      Volume: 11 Pages: 43-76

    • DOI

      10.6092/ISSN.1972-5787/8124

    • Related Report
      2017 Annual Research Report
    • Peer Reviewed / Open Access / Int'l Joint Research
  • [Journal Article] Introduction to Mathematical Components2017

    • Author(s)
      アフェルト レナルド
    • Journal Title

      Computer Software

      Volume: 34 Issue: 2 Pages: 2_64-2_74

    • DOI

      10.11309/jssst.34.2_64

    • NAID

      130006855229

    • ISSN
      0289-6540
    • Related Report
      2016 Annual Research Report
    • Peer Reviewed / Open Access
  • [Presentation] 協調ロボット制御ロジックの設計モデル検証2018

    • Author(s)
      磯部 祥尚
    • Organizer
      第21回CSP研究会
    • Related Report
      2017 Annual Research Report
  • [Presentation] 協調ロボット制御ロジックの形式的なモデル化と検証 - FSM4RTC のための有限状態マシン設計の信頼性向上 -2018

    • Author(s)
      磯部 祥尚, 安藤 慶昭, 宮本 信彦, Biggs Geoffrey, 大岩 寛
    • Organizer
      ロボティクス・メカトロニクス講演会 ROBOMECH2018
    • Related Report
      2017 Annual Research Report
  • [Presentation] Classical analysis with Coq2018

    • Author(s)
      Reynald Affeldt, Cyril Cohen, Assia Mahboubi, Damien Rouhling, and Pierre-Yves Strub
    • Organizer
      The Coq Workshop 2018
    • Related Report
      2017 Annual Research Report
    • Int'l Joint Research
  • [Presentation] FSMコンポーネント実装フレームワークの提案 - FSM4RTC標準に準拠した状態遷移型コンポーネント実装 -2017

    • Author(s)
      安藤 慶昭, 宮本 信彦, 高橋 三郎, ビグズ ジェフ, 花井 亮, 原 功
    • Organizer
      ロボティクス・メカトロニクス講演会 ROBOMECH2017
    • Related Report
      2017 Annual Research Report
  • [Presentation] Formal Foundations of 3D Geometry to Model Robot Manipulators2017

    • Author(s)
      Reynald Affeldt and Cyril Cohen
    • Organizer
      CPP 2017 (The 6th ACM SIGPLAN Conference on Certified Programs and Proofs)
    • Related Report
      2016 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Formal Foundations for Rigid Body Transformation2016

    • Author(s)
      Reynald Affeldt and Cyril Cohen
    • Organizer
      日本ソフトウェア科学会第33回大会
    • Related Report
      2016 Annual Research Report
  • [Presentation] 協調制御のモデル化と解析に向けて2016

    • Author(s)
      磯部 祥尚
    • Organizer
      第17回CSP研究会
    • Related Report
      2016 Annual Research Report
  • [Presentation] 状態遷移コンポーネントとデータポートに関する標準FSM4RTCについて2016

    • Author(s)
      安藤 慶昭
    • Organizer
      第17回計測自動制御学会 システムインテグレーション部門講演会
    • Related Report
      2016 Annual Research Report
  • [Presentation] 暗号プロトコル検証入門2015

    • Author(s)
      磯部祥尚
    • Organizer
      2015年電子情報通信学会 ソサイエティ大会
    • Place of Presentation
      東北大学 川内北キャンパス(宮城県仙台市)
    • Year and Date
      2015-09-09
    • Related Report
      2015 Annual Research Report
  • [Remarks] Formal Foundations of 3D Geometry to ...

    • URL

      https://staff.aist.go.jp/reynald.affeldt/robot/

    • Related Report
      2017 Annual Research Report
  • [Remarks] Formal Foundations for Modeling Robot Manipulators

    • URL

      https://github.com/affeldt-aist/coq-robot

    • Related Report
      2017 Annual Research Report
  • [Remarks] 協調ロボット制御ロジックの形式的なモデル化と検証

    • URL

      https://staff.aist.go.jp/y-isobe/coop-robo/

    • Related Report
      2017 Annual Research Report
  • [Remarks] Formal Foundations of 3D Geometry to ...

    • Related Report
      2016 Annual Research Report
  • [Remarks] https://staff.aist.go.jp/reynald.affeldt/robot/

    • Related Report
      2016 Annual Research Report

URL: 

Published: 2015-04-16   Modified: 2020-03-30  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi