| 研究課題/領域番号 |
19K20249
|
|---|
| 研究種目 |
若手研究
|
| 配分区分 | 基金 |
|---|
| 審査区分 |
小区分60050:ソフトウェア関連
|
|---|
| 研究機関 | 国立研究開発法人宇宙航空研究開発機構 (2022)
国立情報学研究所 (2019-2021) |
|---|
研究代表者 |
小林 努 国立研究開発法人宇宙航空研究開発機構, 研究開発部門, 研究開発員 (10803405)
|
|---|
| 研究期間 (年度) |
2019-04-01 – 2023-03-31
|
| 研究課題ステータス |
完了 (2022年度)
|
| 配分額 *注記 |
4,160千円 (直接経費: 3,200千円、間接経費: 960千円)
2021年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
2020年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
2019年度: 1,690千円 (直接経費: 1,300千円、間接経費: 390千円)
|
|---|
| キーワード | 形式手法 / 段階的詳細化 / 定理証明 / 自己適応ソフトウェア / Internet of Things / 物理情報システム / AI安全性 / ソフトウェア / システムモデリング / Event-B / 自動運転 / RSS / 頑健性 |
|---|
| 研究開始時の研究の概要 |
本研究では、3つの問題の解決のための手法を開発する。
第一に、「体系的に適切な適応を行うには？」という問題の解決のために、整合性を満たすような適応のパターンを定義する。
第二に、「適応時に賢く妥協するには？」という問題の解決のために、パターンに基づいて仕様の証明情報の分析手法を提案し満たせる要求の判断を体系化する。
第三に、「変化のあった側面のみに絞った適応を行うには？」という問題の解決のために、抽象化された仕様の上で行った適応を具体的な仕様に反映する手法を構築する。
|
| 研究成果の概要 |
物理的な対象を制御するソフトウェアに対し、制御器とその環境の形式的なモデルを構築し検証を行う手法は安全性の保証に有効である。中でも、同じ対象に対し複数の抽象度のモデルを構築するアプローチが複雑さ軽減に効果的である。しかし、環境モデルを現実に合わせるために更新し、制御器モデルもそれに合わせて更新する（適応する）必要がある。我々は、多段階の抽象度を持つ制御器の形式モデルの適応に関する研究を行い、センサの不確かさに自動で対処する手法や、自動運転車が安全に目標を達成することを保証するソフトウェアアーキテクチャの構築・検証手法、宇宙機が故障から復帰する手続きの検証のためのモデル作成手法などを提案した。
|
| 研究成果の学術的意義や社会的意義 |
本研究はコンピュータだけでなく人間にも理解・説明可能である形式的モデルの安全な変更・適応という工学的に発展中の工程に対し、多段階の抽象度の視点から切り込み成果を挙げた点で学術的に意義深いと考える。また、実世界で動作するソフトウェアシステムを（一部の研究ではAIを用いたブラックボックスシステムを）対象とし、その安全性を保証しつつ現実の開発問題に対処する手法を提供している点で社会的にも意義深いと考える。
|
