オートマトン的技法を用いた、物理情報システムのための軽量形式検証の量的発展

点击翻译按钮获取中文摘要

まず今年度は、申請者がこれまで行ってきた、ブラックボックス検査と呼ばれる自動テスト手法の量的な拡張に取り組んだ。ブラックボックス検査はテスト対象のシステムを近似するオートマトンの学習と、モデル検査によるオートマトンに対する形式検証を組み合わせることによる、ブラックボックスシステムのためのテスト手法である。ブラックボックス検査は特に近似オートマトンの再利用が可能な場合に効率的なテストが行えることが知られているが、決定的なオートマトンによってシステムの振る舞いを近似するため、確率的システムへの適用が難しいという欠点があった。特に物理情報システムは、例えばシステムの外乱などの確率的な要素が含まれるため、ブラックボックス検査の適用可能範囲が限定的であった。本研究では、テスト対象のマルコフ決定過程による近似と、確率的モデル検査によるその形式検証を組み合わせることにより、ブラックボックス検査を確率的に拡張した。本研究成果をまとめた論文を執筆し、現在査読中である。また、本年度は監視対象となるログを秘匿したままモニタリングすることのできる、秘匿モニタリングについての研究も行なった。物理情報システムの中でも特にIoTシステムのような応用の場合、各機器によって得られた情報をサーバなどに収集し、異常事態の検出などを行うことが広く行われている。一方IoTシステムによって得られる情報は位置情報や生体情報などのプライバシーに関わるものを含むことも多く、モニタリング対象の情報を開示しないことが好ましい。本研究ではトーラス準同型暗号(TFHE)を用いることで、監視対象のログを秘匿したままモニタリングを行うことのできるアルゴリズムを提案し、計算機実験により実時間モニタリングに適用可能であることを示した。本研究の結果をまとめた論文はシステム検証におけるトップ国際会議CAV 2022に採択された。