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