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）の人工衛星において，リアルタイムで実行可能な計算機リソースで当該推論器は実行可能であることが分かった．①②により，次年度で計画している提案手法を用いた時の検査式の質の変化や，検査式の量をスケールさせた場合の計算機リソースを評価するためのベースラインが整った.

为了建立一种逐步设计大量测试方法的方法，我们进行了初步实验，以创建一种检查方法，以识别异常位置而无需使用该方法。此外，使用现有运行时验证方法（R2U2）的估计器是从创建，上载和执行到轨道的卫星的测试公式（OPS-SAT：https：//www.eoportal.org/satellite-missions/ops-sat#overview）和计算机资源的。在1中，在本实验中，当创建一个不使用技术的检查公式以识别异常位置时，很明显，即使从卫星上检测到安装在卫星上的设备中的单个信号的异常，也可以创建10个以上的检查公式，并且为了使它们与另一个信号的相比，并且需要将它们的相比，并且与这些相比，这些信号的相比是相比，这些相当于这些信号的相比，并且相比之下。真正的异常位置没有技术。这表明使用层次结构使用层次结构使用逐步详细信息，使用层次结构构建系统模型，检查公式和证明的方法的有用性。在2中，目前正在分析详细的计算机资源，但是发现推断设备可以在FPGA SOC（MITYSOM-5CSX）计算机资源的当前操作卫星上实时执行。 ①②建立了一个基线，用于评估测试公式的质量变化时，当使用下一个财政年度计划的建议方法和计算机资源时，计算机资源是在测试公式的缩放量时。