| Project/Area Number |
22K11987
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Review Section |
Basic Section 60050:Software-related
|
|---|
| Research Institution | Japan Aerospace EXploration Agency |
|---|
Principal Investigator |
大久保 梨思子 国立研究開発法人宇宙航空研究開発機構, 研究開発部門, 研究開発員 (60837714)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
小林 努 国立研究開発法人宇宙航空研究開発機構, 研究開発部門, 研究開発員 (10803405)
|
|---|
| Project Period (FY) |
2022-04-01 – 2025-03-31
|
| Project Status |
Granted (Fiscal Year 2022)
|
| Budget Amount *help |
¥2,860,000 (Direct Cost: ¥2,200,000、Indirect Cost: ¥660,000)
Fiscal Year 2024: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
Fiscal Year 2023: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2022: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
|
|---|
| Keywords | ソフトウェア / 形式手法 / 異常推論 / ランタイム検証 |
|---|
| Outline of Research at the Start |
形式手法を用いたランタイム検証は，システムの実稼働状況を入力とし，論理式でモデル化された検査式を用い，リアルタイムでシステムの期待する状態からの逸脱を検出する手法である．異常検知とその箇所を特定する機能は複雑になりやすく検証しきれない課題があったが，当該手法では可視性のある検査式で演繹的に推論器の構築ができ，かつ開発時に厳密な検証が可能となる．本研究では，人工衛星を題材に，異常箇所の演繹的推論を実現するため，段階的に検査式の作成とその証明を行いながら，多量の検査式と真の異常箇所の対応関係が取られた推論器を構築する手法を提案する．
|
| Outline of Annual Research Achievements |
多量の検査式を段階的に設計する手法を確立するため，①手法を用いずに異常箇所特定のための検査式を作成することを予備実験的に実施した．また先行し，②作成した検査式から既存のランタイム検証手法（R2U2）を用いた推定器を実装し，軌道上の衛星（OPS-SAT：https://www.eoportal.org/satellite-missions/ops-sat#overview）にアップロードおよび実行し，計算機リソースの計測を実施した．
①において，今回の実験では手法を用いずに異常箇所を特定する検査式を作成する場合，人工衛星に搭載される機器からの単一の信号の異常を検知するだけでも，10以上の検査式が作成可能で，更に異常箇所を特定するためには別の信号との比較等が必要となり，その組み合わせは指数関数的に増えるため，手法なく真の異常箇所との対応関係を取ることが困難となることが明確になった．これにより，段階的詳細化を用い，システムモデル・検査式・証明を抽象から具体への階層構造を用いながら構築していく方法の有用性が示唆された．
②において，詳細な計算機リソースは解析中であるが，現在運用されているFPGA SoC（MitySOM-5CSX）の人工衛星において，リアルタイムで実行可能な計算機リソースで当該推論器は実行可能であることが分かった．
①②により，次年度で計画している提案手法を用いた時の検査式の質の変化や，検査式の量をスケールさせた場合の計算機リソースを評価するためのベースラインが整った.
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
次年度で計画している提案手法を用いた時の有効性（検査式の質の変化等の評価）や，検査式の量をスケールさせた場合の計算機リソースを評価するためのベースラインが整ったため．
|
| Strategy for Future Research Activity |
計画通り，提案した手法で構築した推論器の実装を行い，ランタイム検証が用いる計算機リソースを明らかにし，手法の有効性を評価する．なお，当初計画は実行環境としてFPGA SoC（MitySOM-5CSX）を想定していたが，より現在の人工衛星で一般的なデバイスを用いて実験を行うことも検討している．
|
