Development of Deductive Failure Reasoner with Stepwise Refinement and Theorem Proving

2023 Fiscal Year Annual Research Report

• Project/Area Number: 22K11987
• Research Institution: Japan Aerospace EXploration Agency
• Principal Investigator: 大久保 梨思子 国立研究開発法人宇宙航空研究開発機構, 研究開発部門, 研究開発員 (60837714)
• Co-Investigator(Kenkyū-buntansha): 小林 努 国立研究開発法人宇宙航空研究開発機構, 研究開発部門, 研究開発員 (10803405)
• Project Period (FY): 2022-04-01 – 2024-03-31
• Keywords: ソフトウェア / 形式手法 / 異常推論 / ランタイム検証

Outline of Annual Research Achievements

システムの異常箇所をランタイム検証を用いて推論するための，多量の検査式を段階的に設計する手法を確立するため，①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月から中断している．