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

2020 年度 実績報告書

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

研究課題

研究課題/領域番号 18J22498
研究機関京都大学

研究代表者

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

研究期間 (年度) 2018-04-25 – 2021-03-31
キーワードモニタリング / 軽量形式検証 / 物理情報システム / ハイブリッドオートマトン / 探索的テスト
研究実績の概要

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

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

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

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

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

今後の研究の推進方策

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

  • 研究成果

    (11件)

すべて 2021 2020 その他

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

  • [雑誌論文] Constrained Optimization for Falsification and Conjunctive Synthesis.2021

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

      6th IFAC Conference on Analysis and Design of Hybrid Systems

      巻: - ページ: -

    • 査読あり
  • [雑誌論文] Model-bounded monitoring of hybrid systems2021

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

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

      巻: - ページ: -

    • DOI

      10.1145/3450267.3450531

    • 査読あり / 国際共著
  • [雑誌論文] 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

    • 査読あり / 国際共著
  • [雑誌論文] Falsification of cyber-physical systems with robustness-guided black-box checking.2020

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

      HSCC'20: 23rd ACM International Conference on Hybrid Systems: Computation and Control

      巻: - ページ: 11:1-11:13

    • DOI

      10.1145/3365365.3382193

    • 査読あり
  • [雑誌論文] Weighted Automata Extraction from Recurrent Neural Networks via Regression on State Spaces2020

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

      Proceedings of the AAAI Conference on Artificial Intelligence

      巻: 34 ページ: 5306~5314

    • DOI

      10.1609/aaai.v34i04.5977

    • 査読あり / オープンアクセス / 国際共著
  • [学会発表] Falsification of cyber-physical systems with robustness-guided black-box checking2021

    • 著者名/発表者名
      Masaki Waga
    • 学会等名
      12th ACM/IEEE International Conference on Cyber-Physical Systems
    • 国際学会
  • [学会発表] Symbolic Monitoring against Specifications Parametric in Time and Data2020

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

    • 著者名/発表者名
      Masaki Waga
    • 学会等名
      23rd ACM International Conference on Hybrid Systems: Computation and Control
    • 国際学会
  • [備考] Masaki Waga(和賀 正樹)

    • URL

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

  • [産業財産権] モニタリング装置及びモニタリング方法2020

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

    • 発明者名
      和賀 正樹
    • 権利者名
      和賀 正樹
    • 産業財産権種類
      特許
    • 産業財産権番号
      特願2020-072577

URL: 

公開日: 2021-12-27  

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

Powered by NII kakenhi