Development of Deductive Failure Reasoner with Stepwise Refinement and Theorem Proving

多量の検査式を段階的に設計する手法を確立するため，①手法を用いずに異常箇所特定のための検査式を作成することを予備実験的に実施した．また先行し，②作成した検査式から既存のランタイム検証手法（R2U2）を用いた推定器を実装し，軌道上の衛星（OPS-SAT：https://www.eoportal.org/satellite-missions/ops-sat#overview）にアップロードおよび実行し，計算機リソースの計測を実施した．①において，今回の実験では手法を用いずに異常箇所を特定する検査式を作成する場合，人工衛星に搭載される機器からの単一の信号の異常を検知するだけでも，10以上の検査式が作成可能で，更に異常箇所を特定するためには別の信号との比較等が必要となり，その組み合わせは指数関数的に増えるため，手法なく真の異常箇所との対応関係を取ることが困難となることが明確になった．これにより，段階的詳細化を用い，システムモデル・検査式・証明を抽象から具体への階層構造を用いながら構築していく方法の有用性が示唆された．②において，詳細な計算機リソースは解析中であるが，現在運用されているFPGA SoC（MitySOM-5CSX）の人工衛星において，リアルタイムで実行可能な計算機リソースで当該推論器は実行可能であることが分かった．①②により，次年度で計画している提案手法を用いた時の検査式の質の変化や，検査式の量をスケールさせた場合の計算機リソースを評価するためのベースラインが整った.

多量の検査式を段階的に設計する手法を確立するため，①手法を用いずに異常箇所特定のための検査式を作成することを予備実験的に実施した．また先行し，②作成した検査式から既存のランタイム検証手法（R2U2）を用いた推定器を実装し，軌道上の衛星（OPS-SAT：https://www.eoportal.org/satellite-missions/ops-sat#overview）にアップロードおよび実行し，計算機リソースの計測を実施した．①において，今回の実験では手法を用いずに異常箇所を特定する検査式を作成する場合，人工衛星に搭載される機器からの単一の信号の異常を検知するだけでも，10以上の検査式が作成可能で，更に異常箇所を特定するためには別の信号との比較等が必要となり，その組み合わせは指数関数的に増えるため，手法なく真の異常箇所との対応関係を取ることが困難となることが明確になった．これにより，段階的詳細化を用い，システムモデル・検査式・証明を抽象から具体への階層構造を用いながら構築していく方法の有用性が示唆された．②において，詳細な計算機リソースは解析中であるが，現在運用されているFPGA SoC（MitySOM-5CSX）の人工衛星において，リアルタイムで実行可能な計算機リソースで当該推論器は実行可能であることが分かった．①②により，次年度で計画している提案手法を用いた時の検査式の質の変化や，検査式の量をスケールさせた場合の計算機リソースを評価するためのベースラインが整った.