2018 Fiscal Year Final Research Report

A Development Process of Control Software for Safe Cooperative Robots

Research Project

PDF

Project/Area Number	15H02687
Research Category	Grant-in-Aid for Scientific Research (B)
Allocation Type	Single-year Grants
Section	一般
Research Field	Software
Research Institution	National 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
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.
Free Research Field	形式手法
Academic Significance and Societal Importance of the Research Achievements	大規模IoT化が進むなか、大量のモノが高速で連携する自律・分散・協調システムの重要性が高まりつつある。その一方で、協調動作では発生確率の低いタイミング依存の不具合が潜在化する可能性があり、実装後のテストでは検出しきれないなどの問題がある。本研究では、運動制御と協調制御の形式記述と検証の作業コスト削減可能なライブラリを作成し、ロボットアームと協調搬送ロボットを例として、形式化の効果を示した。産業界への形式手法導入は容易ではないが、本研究のように、その効果と作業コスト削減の可能性を示すことによって、形式手法は今後の自律・分散・協調システムの安全性向上に資する技術となりうる。