| 研究課題/領域番号 |
15H02687
|
|---|
| 研究種目 |
基盤研究(B)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
ソフトウェア
|
|---|
| 研究機関 | 国立研究開発法人産業技術総合研究所 |
|---|
研究代表者 |
磯部 祥尚 国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 主任研究員 (50356458)
|
|---|
| 研究分担者 |
花井 亮 国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 研究員 (10521255)
大岩 寛 国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 研究チーム長 (20415649)
BIGGS Geoffrey 国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 主任研究員 (20534803)
Affeldt Reynald 国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 主任研究員 (40415641)
安藤 慶昭 国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 研究チーム長 (50371018)
中坊 嘉宏 国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 研究チーム長 (70360609)
|
|---|
| 研究期間 (年度) |
2015-04-01 – 2018-03-31
|
| キーワード | 協調ロボット / 制御ソフトウェア / 安全性 / 形式手法 / 検証 / モデル検査 / 定理証明 / 有限状態機械 |
|---|
| 研究成果の概要 |
自律・分散・協調ロボットの制御ソフトウェアの安全性向上を目的として、制御の振舞いを厳密に記述・検証するために形式手法を適用した。その成果は、定理証明器による運動制御の形式検証技術とモデル検査器による協調制御の形式検証技術から成る。運動制御では、ロボットの運動学（キネマティクス）のライブラリを定理証明器Coq上に形式化し、その有効性をロボットアームの形式化・検証に適用して実証した。協調制御では、協調搬送ロボットを例に、設計（有限状態機械）、形式化（仕様記述言語CSP）、検証（モデル検査器FDR）、実装（ミドルウェアRTM）の各工程を連携させ、設計段階で協調動作の不具合を検出できることを示した。
|
| 自由記述の分野 |
形式手法
|
| 研究成果の学術的意義や社会的意義 |
大規模IoT化が進むなか、大量のモノが高速で連携する自律・分散・協調システムの重要性が高まりつつある。その一方で、協調動作では発生確率の低いタイミング依存の不具合が潜在化する可能性があり、実装後のテストでは検出しきれないなどの問題がある。本研究では、運動制御と協調制御の形式記述と検証の作業コスト削減可能なライブラリを作成し、ロボットアームと協調搬送ロボットを例として、形式化の効果を示した。産業界への形式手法導入は容易ではないが、本研究のように、その効果と作業コスト削減の可能性を示すことによって、形式手法は今後の自律・分散・協調システムの安全性向上に資する技術となりうる。
|
