Development of Deductive Failure Reasoner with Stepwise Refinement and Theorem Proving

逐步细化和定理证明的演绎失败推理机的开发

• 批准号: 22K11987
• 负责人: 大久保 梨思子
• 金额: $ 1.83万
• 依托单位: Japan Aerospace EXploration Agency
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (C)
• 财政年份: 2022
• 资助国家: 日本
• 起止时间: 2022-04-01 至 2025-03-31
• 项目状态: 未结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-22K11987/
• 关键词: ソフトウェア; 形式手法; 異常推論; ランタイム検証

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

The design method of multi-stage investigation is established. In addition, ② the inspection formula was created and the existing R2U2 verification method was used, the estimator was installed, the satellite in orbit (OPS-SAT: https://www.eoportal.org/satellite-missions/ops-sat#overview) was implemented, and the computer's smart measurement was implemented. 1. In the case of abnormal signal detection by artificial satellite, more than 10 investigation formulas can be created, and abnormal signal comparison is necessary, and the combination of abnormal signal detection by artificial satellite is necessary. The method is true and the relationship between them is difficult. The detailed structure of the hierarchy is used to demonstrate the usefulness of the method. 2. The detailed computer solutions are analyzed in detail. Now, the FPGA SoC (MitySOM-5CSX) is used to analyze the artificial satellite. The computer solutions are possible when the inference device is implemented. (2) In the next year's plan, the proposal method is used in the middle of the investigation, the quality of the investigation is changed, the quantity of the investigation is changed, and the computer solution is evaluated.