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

使用自动机技术对物理信息系统进行轻量级形式验证的定量开发

• 批准号: 22K17873
• 负责人: 和賀 正樹
• 金额: $ 2.91万
• 依托单位: Kyoto University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Early-Career Scientists
• 财政年份: 2022
• 资助国家: 日本
• 起止时间: 2022-04-01 至 2025-03-31
• 项目状态: 未结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-22K17873/
• 关键词: 能動的MDP学習; 確率的モデル検査; ブラックボックス検査; 準同型暗号; 秘匿モニタリング; 物理情報システム; 軽量形式手法; オートマトン理論; 量的検証

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

This year, the applicant shall select the appropriate group for the amount of information required by the automatic search and call system. The search engine is configured to approximate the object's style and method of learning, searching, and matching the object's style. The search for the best rate of reuse in a particular situation is to approximate the best rate of reuse and determine the best rate of reuse in a particular situation. Special physical information, such as the number of items in the list, and the number of items in the list. This study aims to investigate the approximate and accurate results in the determination process of the target image and to investigate the accuracy of the target image. The results of this research are published in the journal. This year, we will continue to monitor the progress of research and development. The physical information system is composed of special IoT system, application case, machine information collection, abnormal situation detection, etc. The information obtained from one party's IoT system includes location information, biological information, and information about the target. In this study, the use of quasi-isotype code (TFHE), the monitoring of the object, the detection of the object. The results of this study were presented at CAV 2022 International Conference on Science and Technology.

项目成果

Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption

通过全同态加密对安全 LTL 规范进行不经意的在线监控

• DOI: 10.1007/978-3-031-13185-1_22
• 发表时间: 2022
• 期刊: 34th International Conference on Computer-Aided Verification
• 作者: Banno Ryotaro;Matsuoka Kotaro;Matsumoto Naoki;Bian Song;Waga Masaki;Suenaga Kohei
• 通讯作者: Suenaga Kohei

Masaki Waga (和賀 正樹)

和贺正树