物理情報システムに対する軽量検証の、オートマトン的技法を用いた実用的発展

2018 年度 実績報告書

• 研究課題/領域番号: 18J22498
• 研究機関: 総合研究大学院大学
• 研究代表者: 和賀 正樹 総合研究大学院大学, 複合科学研究科, 特別研究員(DC1)
• 研究期間 (年度): 2018-04-25 – 2021-03-31
• キーワード: モニタリング / 物理情報システム / 時間オートマトン / ムーアマシン / パラメタ同定

研究実績の概要

本年度前半は、ネットワークで繋がれている組込みシステムなどにおいて、少ない計算リソースで効率的に時間パターンマッチング問題に対する前処理を行なう、ムーアマシンフィルタを提案・実装し、実験を行った。本研究の結果をまとめた論文は国際会議 EMSOFT 2018に採択され、口頭発表を行い、論文誌 IEEE TCAD に収録されている。本研究については国内学会 PPL 2019にも採択され、口頭発表を行った。

本年度後半は主にフランス・パリ第13大学のEtienne Andre准教授と共に、時間パターンマッチング問題の、入力の仕様がパラメタを含む場合への拡張である、パラメタ付き時間パターンマッチング問題についての研究を行った。まず、パラメタ付き時間パターンマッチング問題を、パラメタ付き時間オートマトンを用いて定式化し、パラメタ付きモデル検査のツールであるIMITATORを用いてパラメタ付き時間パターンマッチング問題を解く手法を提案、実験を行った。本研究の結果をまとめた論文は国際会議 ICECCS 2018に採択され、best paper awardを受賞した。また、(パラメタなし) 時間パターンマッチング問題に対する高速化の手法を、パラメタ付き時間パターンマッチング問題へと拡張する研究も行った。この高速化の手法を用いたアルゴリズムにより、より大きな入力に対して現実的な時間で処理することが可能となった。このアルゴリズムを実装・実験し、結果を論文としてまとめ、国際会議 NFM 2019に採択された。

また、申請者は修士課程在学中に、時間パターンマッチング問題を効率的に解くアルゴリズムをツール MONAA として実装・公開した。この成果は前年度国際ワークショップMT-CPS 2018に投稿され採択されていたが、その口頭発表が本年度申請者によって行われた。

現在までの達成度 (区分)

1: 当初の計画以上に進展している

理由

当初の計画について、計画以上の進展が得られた。まず、当初の研究計画にあった「より本質的な情報を抽出」する手法として、上述のAndre氏と共にパラメタ付き時間パターンマッチング問題を定式化及びアルゴリズムの提案を行ない、トップ国際会議の一つであるICECCS’18 (CORE rank A) に採択され，最優秀論文賞を受けた [Andre, Hasuo & Waga, ICECCS’18]。
さらに、申請者の以前の研究と組み合わせて更なる高速化も達成することができ、NASAの主催する国際会議に採択された[Waga & Andre, NFM’19, accepted]。

また、組込みシステムにおける軽量検証のためのムーアマシンフィルタの提案も行い、組み込みシステム分野のトップ国際会議であるEMSOFT 2018(CORE rank A)において発表された。この成果については特許出願も行った。

今後の研究の推進方策

前年度は「より本質的な情報を抽出」する手法として、パラメタ付き時間パターンマッチング問題について取り組んだ。本年度は、パラメタ付き時間パターンマッチング問題を解くツールの公開を行うとともに、更に多くの情報を抽出できるような手法を構築することを主眼において研究を進める。

また、組込みシステムにおける軽量検証技術についても引き続き改良を進めていく。

研究成果

• [雑誌論文] Online Parametric Timed Pattern Matching with Automata-Based Skipping (2019)
  • 著者名/発表者名: Masaki Waga, Etienne Andre
  • 雑誌名: Proc. NFM 2019, Lecture Notes in Computer Science 巻: 印刷中 ページ: 印刷中
  • 査読あり / 国際共著
• [雑誌論文] Moore-Machine Filtering for Timed and Untimed Pattern Matching (2018)
  • 著者名/発表者名: Masaki Waga, Ichiro Hasuo
  • 雑誌名: IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 巻: 37 ページ: 2649-2660
  • DOI: 10.1109/TCAD.2018.2857358
  • 査読あり
• [雑誌論文] MONAA: a Tool for Timed Pattern Matching with Automata-Based Acceleration (2018)
  • 著者名/発表者名: Masaki Waga, Ichiro Hasuo, Kohei Suenaga
  • 雑誌名: 3rd Workshop on Monitoring and Testing of Cyber-physical Systems (MT-CPS 2018) 巻: － ページ: 14-15
  • DOI: 10.1109/MT-CPS.2018.00014
  • 査読あり
• [雑誌論文] Offline Timed Pattern Matching under Uncertainty (2018)
  • 著者名/発表者名: Andre Etienne、Hasuo Ichiro、Waga Masaki
  • 雑誌名: Proc. ICECCS 2018 巻: － ページ: －
  • DOI: 10.1109/ICECCS2018.2018.00010
  • 査読あり / 国際共著
• [学会発表] Moore-Machine Filtering for Timed and Untimed Pattern Matching (2019)
  • 著者名/発表者名: Masaki Waga
  • 学会等名: 第21回プログラミングおよびプログラミング言語ワークショップ
• [学会発表] Moore-Machine Filtering for Timed and Untimed Pattern Matching (2018)
  • 著者名/発表者名: Masaki Waga
  • 学会等名: 2018 International Conference on Embedded Software
  • 国際学会
• [学会発表] MONAA: a Tool for Timed Pattern Matching with Automata-Based Acceleration (2018)
  • 著者名/発表者名: Masaki Waga
  • 学会等名: 3rd Workshop on Monitoring and Testing of Cyber-physical Systems
  • 国際学会
• [備考] 申請者個人ウェブページ
  • URL: http://group-mmm.org/~mwaga/
• [産業財産権] 情報処理装置、情報処理システム及び情報処理方法 (2018)
  • 発明者名: 和賀 正樹、蓮尾 一郎
  • 権利者名: 和賀 正樹、蓮尾 一郎
  • 産業財産権種類: 特許
  • 産業財産権番号: Ｐ２６１０９４