• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 課題ページに戻る

2023 年度 実績報告書

段階的詳細化と定理証明を用いた演繹的なリアルタイム異常箇所推論器の構築

研究課題

研究課題/領域番号 22K11987
研究機関国立研究開発法人宇宙航空研究開発機構

研究代表者

大久保 梨思子  国立研究開発法人宇宙航空研究開発機構, 研究開発部門, 研究開発員 (60837714)

研究分担者 小林 努  国立研究開発法人宇宙航空研究開発機構, 研究開発部門, 研究開発員 (10803405)
研究期間 (年度) 2022-04-01 – 2024-03-31
キーワードソフトウェア / 形式手法 / 異常推論 / ランタイム検証
研究実績の概要

システムの異常箇所をランタイム検証を用いて推論するための,多量の検査式を段階的に設計する手法を確立するため,①2022年度に予備実験的に行った人工衛星での推論の結果分析および②予備実験に基づく提案手法の検討を実施した.
①に関して,ラインタイム検証が使う計算機リソースについて,軌道上で運用されている人工衛星(OPS-SAT: https://www.eoportal.org/satellitemissions/
ops-sat#overview)を用い,予備実験的に製作したランタイム検証の推論器を実行した.本年度は,当該実行結果の詳細を分析した.本研究課題で採用したランタイム検証の手法(R2U2)が,10程度の検査式を用いて推論した場合,FPGA SoC(MitySOM-5CSX)およびyocto linux OSレベルでの計測という前提において,平均38.6MB程度(10秒間隔での計測)のメモリ消費量で実行されていたことを明らかにした.
②に関して,2022年度の予備実験の結果から,異常箇所を特定するためには別の信号との比較等が必要となり,その組み合わせは指数関数的に増えるため,手法なく真の異常箇所との対応関係を取ることが困難となることが明確になった.本年度は,真の異常箇所と検査式の対応関係を取るための入力情報として必要な,既知の人工衛星の異常状態とその原因(本研究課題の推論対象)を段階的詳細化で利用しやすい形で蓄積する方法を検討および提案した.具体的には,既知の異常状態を抽象から具体に木構造的に整理し,また段階的詳細化におけるシステムモデルとの対応をつけやすくなるようなシステムの文脈(コンテキスト)を付加している.
本研究課題は研究代表者が海外における研究滞在を行うため,2024年1月から中断している.

URL: 

公開日: 2024-12-25  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi