• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 前のページに戻る

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

研究課題

研究課題/領域番号 18J22498
研究種目

特別研究員奨励費

配分区分補助金
応募区分国内
研究分野 ソフトウェア
研究機関京都大学 (2020)
総合研究大学院大学 (2018-2019)

研究代表者

和賀 正樹  京都大学, 情報学研究科, 助教

研究期間 (年度) 2018-04-25 – 2021-03-31
研究課題ステータス 完了 (2020年度)
配分額 *注記
2,200千円 (直接経費: 2,200千円)
2020年度: 700千円 (直接経費: 700千円)
2019年度: 700千円 (直接経費: 700千円)
2018年度: 800千円 (直接経費: 800千円)
キーワードモニタリング / 軽量形式検証 / 物理情報システム / ハイブリッドオートマトン / 探索的テスト / 反例生成 / 時間オートマトン / パラメタ同定 / オートマトン学習 / 回帰型ニューラルネットワーク / ムーアマシン
研究実績の概要

まず本年度は、モニタリング対象のシステムの近似的な動作の仮定を用いたモニタリング問題の拡張を行った。具体的には線形ハイブリッドオートマトンで与えられたシステムに近似モデルを用いることで、間欠的にサンプリオングされたログにおいて、二つのサンプルの間での動作についてもモニタリングを行うことができる拡張を行った。このことにより、例えば異常動作の検出漏れを防ぎつつサンプリング周期を伸ばすことが可能となり、組込みシステム等計算資源が限られている環境での応用が期待できる。本研究結果をまとめた論文が物理情報システムに関する国際会議 ICCPS 2021に採択された。

さらに物理情報システムの探索的テストにおける、異なる物理量に言及したさいの困難を解決する研究も行った。異なる物理量間では通常用いられる値の大きさが一般には異なるが、これによって物理情報システムの探索的テストにおいて、ある特定の物理量の変化が事実上無視されてしまうという「スケール問題」という現象が知られていた。本研究では、物理量の絶対的な大きさのみではなく相対的な順位も考慮することで、「スケール問題」を回避しながら探索的テストを行うことのできる拡張を行った。本研究結果をまとめた論文がシステム制御に関する国際会議 ADHS 2021に採択された。

また、前年度に採択された、物理情報システムについての反例生成問題を、オートマトン学習を経由して解く手法について研究成果を物理情報システムに関する国際会議HSCC 2020において口頭発表を行った。更に日本ソフトウェア科学会第37回大会において、前年度に研究を行った[Waga, Andre, & Hasuo, CAV'19]の内容について招待講演を行った。
また,前々年度,前年度,本年度の成果を博士論文として体系化した.

現在までの達成度 (段落)

令和2年度が最終年度であるため、記入しない。

今後の研究の推進方策

令和2年度が最終年度であるため、記入しない。

報告書

(3件)
  • 2020 実績報告書
  • 2019 実績報告書
  • 2018 実績報告書
  • 研究成果

    (33件)

すべて 2021 2020 2019 2018 その他

すべて 国際共同研究 (1件) 雑誌論文 (15件) (うち国際共著 8件、 査読あり 15件、 オープンアクセス 4件) 学会発表 (11件) (うち国際学会 9件、 招待講演 1件) 備考 (3件) 産業財産権 (3件)

  • [国際共同研究] パリ13大学/ロレーヌ大学(フランス)

    • 関連する報告書
      2019 実績報告書
  • [雑誌論文] Constrained Optimization for Falsification and Conjunctive Synthesis.2021

    • 著者名/発表者名
      Sato Sota、Waga Masaki、Hasuo Ichiro
    • 雑誌名

      6th IFAC Conference on Analysis and Design of Hybrid Systems

      巻: -

    • 関連する報告書
      2020 実績報告書
    • 査読あり
  • [雑誌論文] Model-bounded monitoring of hybrid systems2021

    • 著者名/発表者名
      Waga Masaki、Andre Etienne、Hasuo Ichiro
    • 雑誌名

      12th ACM/IEEE International Conference on Cyber-Physical Systems

      巻: - ページ: 21-32

    • DOI

      10.1145/3450267.3450531

    • 関連する報告書
      2020 実績報告書
    • 査読あり / 国際共著
  • [雑誌論文] Genetic algorithm for the weight maximization problem on weighted automata2020

    • 著者名/発表者名
      Gutierrez Elena、Okudono Takamasa、Waga Masaki、Hasuo Ichiro
    • 雑誌名

      GECCO'20: Genetic and Evolutionary Computation Conference

      巻: - ページ: 699-707

    • DOI

      10.1145/3377930.3390227

    • 関連する報告書
      2020 実績報告書
    • 査読あり / 国際共著
  • [雑誌論文] Falsification of Cyber-Physical Systems with Robustness-Guided Black-Box Checking2020

    • 著者名/発表者名
      Masaki Waga
    • 雑誌名

      Proc. HSCC 2020, 23rd ACM International Conference on Hybrid Systems: Computation and Control

      巻: - ページ: 1-13

    • DOI

      10.1145/3365365.3382193

    • 関連する報告書
      2020 実績報告書
    • 査読あり
  • [雑誌論文] Weighted Automata Extraction from Recurrent Neural Networks via Regression on State Spaces2020

    • 著者名/発表者名
      Takamasa Okudono, Masaki Waga, Taro Sekiyama, Ichiro Hasuo
    • 雑誌名

      Proceedings of AAAI Conference on Artificial Intelligence (AAAI)

      巻: 34 号: 04 ページ: 5306-5314

    • DOI

      10.1609/aaai.v34i04.5977

    • 関連する報告書
      2020 実績報告書
    • 査読あり / オープンアクセス / 国際共著
  • [雑誌論文] Genetic Algorithm for the Weight Maximization Problem on Weighted Automata2020

    • 著者名/発表者名
      Elena Gutierrez, Takamasa Okudono, Masaki Waga, Ichiro Hasuo
    • 雑誌名

      Proc. GECCO 2020, The Genetic and Evolutionary Computation Conference

      巻: -

    • 関連する報告書
      2019 実績報告書
    • 査読あり / オープンアクセス / 国際共著
  • [雑誌論文] Weighted Automata Extraction from Recurrent Neural Networks via Regression on State Spaces2020

    • 著者名/発表者名
      Takamasa Okudono, Masaki Waga, Taro Sekiyama, Ichiro Hasuo
    • 雑誌名

      Proc. AAAI 2020, Thirty-Fourth AAAI Conference on Artificial Intelligence

      巻: -

    • 関連する報告書
      2019 実績報告書
    • 査読あり / オープンアクセス
  • [雑誌論文] Falsification of Cyber-Physical Systems with Robustness-Guided Black-Box Checking2020

    • 著者名/発表者名
      Masaki Waga
    • 雑誌名

      Proc. HSCC 2020, 23rd ACM International Conference on Hybrid Systems: Computation and Control

      巻: -

    • 関連する報告書
      2019 実績報告書
    • 査読あり
  • [雑誌論文] Online Quantitative Timed Pattern Matching with Semiring-Valued Weighted Automata2019

    • 著者名/発表者名
      Waga Masaki
    • 雑誌名

      Proc. FORMATS 2019, 17th International Conference on Formal Modeling and Analysis of Timed Systems

      巻: 11750 ページ: 3-22

    • DOI

      10.1007/978-3-030-29662-9_1

    • ISBN
      9783030296612, 9783030296629
    • 関連する報告書
      2019 実績報告書
    • 査読あり
  • [雑誌論文] Symbolic Monitoring against Specifications Parametric in Time and Data2019

    • 著者名/発表者名
      Masaki Waga, Eienne Andre, Ichiro Hasuo
    • 雑誌名

      Proc. CAV 2019, 31st International Conference on Computer Aided Verification

      巻: 11561 ページ: 520-539

    • DOI

      10.1007/978-3-030-25540-4_30

    • ISBN
      9783030255398, 9783030255404
    • 関連する報告書
      2019 実績報告書
    • 査読あり / オープンアクセス / 国際共著
  • [雑誌論文] Online Parametric Timed Pattern Matching with Automata-Based Skipping2019

    • 著者名/発表者名
      Masaki Waga, Eienne Andre
    • 雑誌名

      Proc. NFM 2019, 11th Annual NASA Formal Methods Symposium

      巻: 11460 ページ: 371-389

    • DOI

      10.1007/978-3-030-20652-9_26

    • ISBN
      9783030206512, 9783030206529
    • 関連する報告書
      2019 実績報告書
    • 査読あり / 国際共著
  • [雑誌論文] Online Parametric Timed Pattern Matching with Automata-Based Skipping2019

    • 著者名/発表者名
      Masaki Waga, Etienne Andre
    • 雑誌名

      Proc. NFM 2019, Lecture Notes in Computer Science

      巻: 印刷中

    • 関連する報告書
      2018 実績報告書
    • 査読あり / 国際共著
  • [雑誌論文] Moore-Machine Filtering for Timed and Untimed Pattern Matching2018

    • 著者名/発表者名
      Masaki Waga, Ichiro Hasuo
    • 雑誌名

      Proc. EMSOFT 2018, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems

      巻: 37 号: 11 ページ: 2649-2660

    • DOI

      10.1109/tcad.2018.2857358

    • 関連する報告書
      2018 実績報告書
    • 査読あり
  • [雑誌論文] MONAA: a Tool for Timed Pattern Matching with Automata-Based Acceleration2018

    • 著者名/発表者名
      Masaki Waga, Ichiro Hasuo, Kohei Suenaga
    • 雑誌名

      Proc. MT-CPS 2018

      巻: - ページ: 14-15

    • DOI

      10.1109/mt-cps.2018.00014

    • 関連する報告書
      2018 実績報告書
    • 査読あり
  • [雑誌論文] Offline Timed Pattern Matching under Uncertainty2018

    • 著者名/発表者名
      Andre Etienne、Hasuo Ichiro、Waga Masaki
    • 雑誌名

      Proc. ICECCS 2018

      巻: - ページ: 10-20

    • DOI

      10.1109/iceccs2018.2018.00010

    • 関連する報告書
      2018 実績報告書
    • 査読あり / 国際共著
  • [学会発表] Falsification of cyber-physical systems with robustness-guided black-box checking2021

    • 著者名/発表者名
      Masaki Waga
    • 学会等名
      12th ACM/IEEE International Conference on Cyber-Physical Systems
    • 関連する報告書
      2020 実績報告書
    • 国際学会
  • [学会発表] Symbolic Monitoring against Specifications Parametric in Time and Data2020

    • 著者名/発表者名
      和賀 正樹
    • 学会等名
      日本ソフトウェア科学会第37回大会
    • 関連する報告書
      2020 実績報告書
    • 招待講演
  • [学会発表] Falsification of cyber-physical systems with robustness-guided black-box checking2020

    • 著者名/発表者名
      Masaki Waga
    • 学会等名
      23rd ACM International Conference on Hybrid Systems: Computation and Control
    • 関連する報告書
      2020 実績報告書
    • 国際学会
  • [学会発表] Falsification of Cyber-Physical Systems with Robustness-Guided Black-Box Checking2020

    • 著者名/発表者名
      Masaki Waga
    • 学会等名
      23rd ACM International Conference on Hybrid Systems: Computation and Control
    • 関連する報告書
      2019 実績報告書
    • 国際学会
  • [学会発表] Online Quantitative Timed Pattern Matching with Semiring-Valued Weighted Automata2019

    • 著者名/発表者名
      Masaki Waga
    • 学会等名
      17th International Conference on Formal Modeling and Analysis of Timed Systems
    • 関連する報告書
      2019 実績報告書
    • 国際学会
  • [学会発表] Symbolic Monitoring Against Specifications Parametric in Time and Data2019

    • 著者名/発表者名
      Masaki Waga
    • 学会等名
      31st International Conference on Computer-Aided Verification
    • 関連する報告書
      2019 実績報告書
    • 国際学会
  • [学会発表] Moore-Machine Filtering for Timed and Untimed Pattern Matching2019

    • 著者名/発表者名
      Masaki Waga
    • 学会等名
      第21回プログラミングおよびプログラミング言語ワークショップ
    • 関連する報告書
      2019 実績報告書 2018 実績報告書
  • [学会発表] Online Parametric Timed Pattern Matching with Automata-Based Skipping2019

    • 著者名/発表者名
      Masaki Waga
    • 学会等名
      4th Workshop on Monitoring and Testing of Cyber-physical Systems
    • 関連する報告書
      2019 実績報告書
    • 国際学会
  • [学会発表] Online Parametric Timed Pattern Matching with Automata-Based Skipping2019

    • 著者名/発表者名
      Masaki Waga
    • 学会等名
      11th Annual NASA Formal Methods Symposium
    • 関連する報告書
      2019 実績報告書
    • 国際学会
  • [学会発表] Moore-Machine Filtering for Timed and Untimed Pattern Matching2018

    • 著者名/発表者名
      Masaki Waga
    • 学会等名
      2018 International Conference on Embedded Software
    • 関連する報告書
      2018 実績報告書
    • 国際学会
  • [学会発表] MONAA: a Tool for Timed Pattern Matching with Automata-Based Acceleration2018

    • 著者名/発表者名
      Masaki Waga
    • 学会等名
      3rd Workshop on Monitoring and Testing of Cyber-physical Systems
    • 関連する報告書
      2018 実績報告書
    • 国際学会
  • [備考] Masaki Waga(和賀 正樹)

    • URL

      https://www.fos.kuis.kyoto-u.ac.jp/~mwaga/

    • 関連する報告書
      2020 実績報告書
  • [備考] Masaki Waga (和賀 正樹)

    • URL

      http://group-mmm.org/~mwaga/

    • 関連する報告書
      2019 実績報告書
  • [備考] 申請者個人ウェブページ

    • URL

      http://group-mmm.org/~mwaga/

    • 関連する報告書
      2018 実績報告書
  • [産業財産権] モニタリング装置及びモニタリング方法2020

    • 発明者名
      和賀 正樹、エティエンヌ アンドレ、蓮尾 一郎
    • 権利者名
      和賀 正樹、エティエンヌ アンドレ、蓮尾 一郎
    • 産業財産権種類
      特許
    • 産業財産権番号
      2020-215603
    • 出願年月日
      2020
    • 関連する報告書
      2020 実績報告書
  • [産業財産権] オートマトン生成装置、オートマトン生成方法及びプログラム2020

    • 発明者名
      和賀 正樹
    • 権利者名
      和賀 正樹
    • 産業財産権種類
      特許
    • 産業財産権番号
      2020-072577
    • 出願年月日
      2020
    • 関連する報告書
      2020 実績報告書
  • [産業財産権] 情報処理装置、情報処理システム及び情報処理方法2018

    • 発明者名
      和賀 正樹、蓮尾 一郎
    • 権利者名
      和賀 正樹、蓮尾 一郎
    • 産業財産権種類
      特許
    • 出願年月日
      2018
    • 関連する報告書
      2018 実績報告書

URL: 

公開日: 2018-05-01   更新日: 2024-03-26  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi