| 研究課題/領域番号 |
22K11987
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分60050:ソフトウェア関連
|
|---|
| 研究機関 | 国立研究開発法人宇宙航空研究開発機構 |
|---|
研究代表者 |
大久保 梨思子 国立研究開発法人宇宙航空研究開発機構, 研究開発部門, 研究開発員 (60837714)
|
|---|
| 研究分担者 |
小林 努 国立研究開発法人宇宙航空研究開発機構, 研究開発部門, 研究開発員 (10803405)
|
|---|
| 研究期間 (年度) |
2022-04-01 – 2024-03-31
|
| 研究課題ステータス |
完了 (2023年度)
|
| 配分額 *注記 |
2,860千円 (直接経費: 2,200千円、間接経費: 660千円)
2024年度: 650千円 (直接経費: 500千円、間接経費: 150千円)
2023年度: 780千円 (直接経費: 600千円、間接経費: 180千円)
2022年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
|
|---|
| キーワード | ソフトウェア / 形式手法 / 異常推論 / ランタイム検証 |
|---|
| 研究開始時の研究の概要 |
形式手法を用いたランタイム検証は，システムの実稼働状況を入力とし，論理式でモデル化された検査式を用い，リアルタイムでシステムの期待する状態からの逸脱を検出する手法である．異常検知とその箇所を特定する機能は複雑になりやすく検証しきれない課題があったが，当該手法では可視性のある検査式で演繹的に推論器の構築ができ，かつ開発時に厳密な検証が可能となる．本研究では，人工衛星を題材に，異常箇所の演繹的推論を実現するため，段階的に検査式の作成とその証明を行いながら，多量の検査式と真の異常箇所の対応関係が取られた推論器を構築する手法を提案する．
|
| 研究実績の概要 |
システムの異常箇所をランタイム検証を用いて推論するための，多量の検査式を段階的に設計する手法を確立するため，①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月から中断している．
|
