| 研究課題/領域番号 |
22K11987
|
|---|
| 研究機関 | 国立研究開発法人宇宙航空研究開発機構 |
|---|
研究代表者 |
大久保 梨思子 国立研究開発法人宇宙航空研究開発機構, 研究開発部門, 研究開発員 (60837714)
|
|---|
| 研究分担者 |
小林 努 国立研究開発法人宇宙航空研究開発機構, 研究開発部門, 研究開発員 (10803405)
|
|---|
| 研究期間 (年度) |
2022-04-01 – 2025-03-31
|
| キーワード | ソフトウェア / 形式手法 / 異常推論 / ランタイム検証 |
|---|
| 研究実績の概要 |
多量の検査式を段階的に設計する手法を確立するため，①手法を用いずに異常箇所特定のための検査式を作成することを予備実験的に実施した．また先行し，②作成した検査式から既存のランタイム検証手法（R2U2）を用いた推定器を実装し，軌道上の衛星（OPS-SAT：https://www.eoportal.org/satellite-missions/ops-sat#overview）にアップロードおよび実行し，計算機リソースの計測を実施した．
①において，今回の実験では手法を用いずに異常箇所を特定する検査式を作成する場合，人工衛星に搭載される機器からの単一の信号の異常を検知するだけでも，10以上の検査式が作成可能で，更に異常箇所を特定するためには別の信号との比較等が必要となり，その組み合わせは指数関数的に増えるため，手法なく真の異常箇所との対応関係を取ることが困難となることが明確になった．これにより，段階的詳細化を用い，システムモデル・検査式・証明を抽象から具体への階層構造を用いながら構築していく方法の有用性が示唆された．
②において，詳細な計算機リソースは解析中であるが，現在運用されているFPGA SoC（MitySOM-5CSX）の人工衛星において，リアルタイムで実行可能な計算機リソースで当該推論器は実行可能であることが分かった．
①②により，次年度で計画している提案手法を用いた時の検査式の質の変化や，検査式の量をスケールさせた場合の計算機リソースを評価するためのベースラインが整った.
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
次年度で計画している提案手法を用いた時の有効性（検査式の質の変化等の評価）や，検査式の量をスケールさせた場合の計算機リソースを評価するためのベースラインが整ったため．
|
| 今後の研究の推進方策 |
計画通り，提案した手法で構築した推論器の実装を行い，ランタイム検証が用いる計算機リソースを明らかにし，手法の有効性を評価する．なお，当初計画は実行環境としてFPGA SoC（MitySOM-5CSX）を想定していたが，より現在の人工衛星で一般的なデバイスを用いて実験を行うことも検討している．
|
| 次年度使用額が生じた理由 |
当初計画していた旅費について，コロナウイルス感染症対策により国際会議への参加が見送られたため．当該助成金は翌年度分の助成金と合わせ，当初計画にはなかったランタイム検証を実行するためのハードウェア購入等への使用を計画している．
|
