| 研究課題/領域番号 |
19K20249
|
|---|
| 研究種目 |
若手研究
|
| 配分区分 | 基金 |
|---|
| 審査区分 |
小区分60050:ソフトウェア関連
|
|---|
| 研究機関 | 国立研究開発法人宇宙航空研究開発機構 (2022)
国立情報学研究所 (2019-2021) |
|---|
研究代表者 |
小林 努 国立研究開発法人宇宙航空研究開発機構, 研究開発部門, 研究開発員 (10803405)
|
|---|
| 研究期間 (年度) |
2019-04-01 – 2023-03-31
|
| キーワード | 形式手法 / 段階的詳細化 / 定理証明 / 自己適応ソフトウェア / Internet of Things / 物理情報システム / AI安全性 |
|---|
| 研究成果の概要 |
物理的な対象を制御するソフトウェアに対し、制御器とその環境の形式的なモデルを構築し検証を行う手法は安全性の保証に有効である。中でも、同じ対象に対し複数の抽象度のモデルを構築するアプローチが複雑さ軽減に効果的である。しかし、環境モデルを現実に合わせるために更新し、制御器モデルもそれに合わせて更新する（適応する）必要がある。我々は、多段階の抽象度を持つ制御器の形式モデルの適応に関する研究を行い、センサの不確かさに自動で対処する手法や、自動運転車が安全に目標を達成することを保証するソフトウェアアーキテクチャの構築・検証手法、宇宙機が故障から復帰する手続きの検証のためのモデル作成手法などを提案した。
|
| 自由記述の分野 |
ソフトウェア工学
|
| 研究成果の学術的意義や社会的意義 |
本研究はコンピュータだけでなく人間にも理解・説明可能である形式的モデルの安全な変更・適応という工学的に発展中の工程に対し、多段階の抽象度の視点から切り込み成果を挙げた点で学術的に意義深いと考える。また、実世界で動作するソフトウェアシステムを（一部の研究ではAIを用いたブラックボックスシステムを）対象とし、その安全性を保証しつつ現実の開発問題に対処する手法を提供している点で社会的にも意義深いと考える。
|
