• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

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

Research Project

Project/Area Number 18J22498
Research Category

Grant-in-Aid for JSPS Fellows

Allocation TypeSingle-year Grants
Section国内
Research Field Software
Research InstitutionKyoto University (2020)
The Graduate University for Advanced Studies (2018-2019)

Principal Investigator

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

Project Period (FY) 2018-04-25 – 2021-03-31
Project Status Completed (Fiscal Year 2020)
Budget Amount *help
¥2,200,000 (Direct Cost: ¥2,200,000)
Fiscal Year 2020: ¥700,000 (Direct Cost: ¥700,000)
Fiscal Year 2019: ¥700,000 (Direct Cost: ¥700,000)
Fiscal Year 2018: ¥800,000 (Direct Cost: ¥800,000)
Keywordsモニタリング / 軽量形式検証 / 物理情報システム / ハイブリッドオートマトン / 探索的テスト / 反例生成 / 時間オートマトン / パラメタ同定 / オートマトン学習 / 回帰型ニューラルネットワーク / ムーアマシン
Outline of Annual Research Achievements

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

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

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

Research Progress Status

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

Strategy for Future Research Activity

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

Report

(3 results)
  • 2020 Annual Research Report
  • 2019 Annual Research Report
  • 2018 Annual Research Report
  • Research Products

    (33 results)

All 2021 2020 2019 2018 Other

All Int'l Joint Research (1 results) Journal Article (15 results) (of which Int'l Joint Research: 8 results,  Peer Reviewed: 15 results,  Open Access: 4 results) Presentation (11 results) (of which Int'l Joint Research: 9 results,  Invited: 1 results) Remarks (3 results) Patent(Industrial Property Rights) (3 results)

  • [Int'l Joint Research] パリ13大学/ロレーヌ大学(フランス)

    • Related Report
      2019 Annual Research Report
  • [Journal Article] Constrained Optimization for Falsification and Conjunctive Synthesis.2021

    • Author(s)
      Sato Sota、Waga Masaki、Hasuo Ichiro
    • Journal Title

      6th IFAC Conference on Analysis and Design of Hybrid Systems

      Volume: -

    • Related Report
      2020 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Model-bounded monitoring of hybrid systems2021

    • Author(s)
      Waga Masaki、Andre Etienne、Hasuo Ichiro
    • Journal Title

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

      Volume: - Pages: 21-32

    • DOI

      10.1145/3450267.3450531

    • Related Report
      2020 Annual Research Report
    • Peer Reviewed / Int'l Joint Research
  • [Journal Article] Genetic algorithm for the weight maximization problem on weighted automata2020

    • Author(s)
      Gutierrez Elena、Okudono Takamasa、Waga Masaki、Hasuo Ichiro
    • Journal Title

      GECCO'20: Genetic and Evolutionary Computation Conference

      Volume: - Pages: 699-707

    • DOI

      10.1145/3377930.3390227

    • Related Report
      2020 Annual Research Report
    • Peer Reviewed / Int'l Joint Research
  • [Journal Article] Falsification of Cyber-Physical Systems with Robustness-Guided Black-Box Checking2020

    • Author(s)
      Masaki Waga
    • Journal Title

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

      Volume: - Pages: 1-13

    • DOI

      10.1145/3365365.3382193

    • Related Report
      2020 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Weighted Automata Extraction from Recurrent Neural Networks via Regression on State Spaces2020

    • Author(s)
      Takamasa Okudono, Masaki Waga, Taro Sekiyama, Ichiro Hasuo
    • Journal Title

      Proceedings of AAAI Conference on Artificial Intelligence (AAAI)

      Volume: 34 Issue: 04 Pages: 5306-5314

    • DOI

      10.1609/aaai.v34i04.5977

    • Related Report
      2020 Annual Research Report
    • Peer Reviewed / Open Access / Int'l Joint Research
  • [Journal Article] Genetic Algorithm for the Weight Maximization Problem on Weighted Automata2020

    • Author(s)
      Elena Gutierrez, Takamasa Okudono, Masaki Waga, Ichiro Hasuo
    • Journal Title

      Proc. GECCO 2020, The Genetic and Evolutionary Computation Conference

      Volume: -

    • Related Report
      2019 Annual Research Report
    • Peer Reviewed / Open Access / Int'l Joint Research
  • [Journal Article] Weighted Automata Extraction from Recurrent Neural Networks via Regression on State Spaces2020

    • Author(s)
      Takamasa Okudono, Masaki Waga, Taro Sekiyama, Ichiro Hasuo
    • Journal Title

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

      Volume: -

    • Related Report
      2019 Annual Research Report
    • Peer Reviewed / Open Access
  • [Journal Article] Falsification of Cyber-Physical Systems with Robustness-Guided Black-Box Checking2020

    • Author(s)
      Masaki Waga
    • Journal Title

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

      Volume: -

    • Related Report
      2019 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Online Quantitative Timed Pattern Matching with Semiring-Valued Weighted Automata2019

    • Author(s)
      Waga Masaki
    • Journal Title

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

      Volume: 11750 Pages: 3-22

    • DOI

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

    • ISBN
      9783030296612, 9783030296629
    • Related Report
      2019 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Symbolic Monitoring against Specifications Parametric in Time and Data2019

    • Author(s)
      Masaki Waga, Eienne Andre, Ichiro Hasuo
    • Journal Title

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

      Volume: 11561 Pages: 520-539

    • DOI

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

    • ISBN
      9783030255398, 9783030255404
    • Related Report
      2019 Annual Research Report
    • Peer Reviewed / Open Access / Int'l Joint Research
  • [Journal Article] Online Parametric Timed Pattern Matching with Automata-Based Skipping2019

    • Author(s)
      Masaki Waga, Eienne Andre
    • Journal Title

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

      Volume: 11460 Pages: 371-389

    • DOI

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

    • ISBN
      9783030206512, 9783030206529
    • Related Report
      2019 Annual Research Report
    • Peer Reviewed / Int'l Joint Research
  • [Journal Article] Online Parametric Timed Pattern Matching with Automata-Based Skipping2019

    • Author(s)
      Masaki Waga, Etienne Andre
    • Journal Title

      Proc. NFM 2019, Lecture Notes in Computer Science

      Volume: 印刷中

    • Related Report
      2018 Annual Research Report
    • Peer Reviewed / Int'l Joint Research
  • [Journal Article] Moore-Machine Filtering for Timed and Untimed Pattern Matching2018

    • Author(s)
      Masaki Waga, Ichiro Hasuo
    • Journal Title

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

      Volume: 37 Issue: 11 Pages: 2649-2660

    • DOI

      10.1109/tcad.2018.2857358

    • Related Report
      2018 Annual Research Report
    • Peer Reviewed
  • [Journal Article] MONAA: a Tool for Timed Pattern Matching with Automata-Based Acceleration2018

    • Author(s)
      Masaki Waga, Ichiro Hasuo, Kohei Suenaga
    • Journal Title

      Proc. MT-CPS 2018

      Volume: - Pages: 14-15

    • DOI

      10.1109/mt-cps.2018.00014

    • Related Report
      2018 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Offline Timed Pattern Matching under Uncertainty2018

    • Author(s)
      Andre Etienne、Hasuo Ichiro、Waga Masaki
    • Journal Title

      Proc. ICECCS 2018

      Volume: - Pages: 10-20

    • DOI

      10.1109/iceccs2018.2018.00010

    • Related Report
      2018 Annual Research Report
    • Peer Reviewed / Int'l Joint Research
  • [Presentation] Falsification of cyber-physical systems with robustness-guided black-box checking2021

    • Author(s)
      Masaki Waga
    • Organizer
      12th ACM/IEEE International Conference on Cyber-Physical Systems
    • Related Report
      2020 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Symbolic Monitoring against Specifications Parametric in Time and Data2020

    • Author(s)
      和賀 正樹
    • Organizer
      日本ソフトウェア科学会第37回大会
    • Related Report
      2020 Annual Research Report
    • Invited
  • [Presentation] Falsification of cyber-physical systems with robustness-guided black-box checking2020

    • Author(s)
      Masaki Waga
    • Organizer
      23rd ACM International Conference on Hybrid Systems: Computation and Control
    • Related Report
      2020 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Falsification of Cyber-Physical Systems with Robustness-Guided Black-Box Checking2020

    • Author(s)
      Masaki Waga
    • Organizer
      23rd ACM International Conference on Hybrid Systems: Computation and Control
    • Related Report
      2019 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Online Quantitative Timed Pattern Matching with Semiring-Valued Weighted Automata2019

    • Author(s)
      Masaki Waga
    • Organizer
      17th International Conference on Formal Modeling and Analysis of Timed Systems
    • Related Report
      2019 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Symbolic Monitoring Against Specifications Parametric in Time and Data2019

    • Author(s)
      Masaki Waga
    • Organizer
      31st International Conference on Computer-Aided Verification
    • Related Report
      2019 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Moore-Machine Filtering for Timed and Untimed Pattern Matching2019

    • Author(s)
      Masaki Waga
    • Organizer
      第21回プログラミングおよびプログラミング言語ワークショップ
    • Related Report
      2019 Annual Research Report 2018 Annual Research Report
  • [Presentation] Online Parametric Timed Pattern Matching with Automata-Based Skipping2019

    • Author(s)
      Masaki Waga
    • Organizer
      4th Workshop on Monitoring and Testing of Cyber-physical Systems
    • Related Report
      2019 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Online Parametric Timed Pattern Matching with Automata-Based Skipping2019

    • Author(s)
      Masaki Waga
    • Organizer
      11th Annual NASA Formal Methods Symposium
    • Related Report
      2019 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Moore-Machine Filtering for Timed and Untimed Pattern Matching2018

    • Author(s)
      Masaki Waga
    • Organizer
      2018 International Conference on Embedded Software
    • Related Report
      2018 Annual Research Report
    • Int'l Joint Research
  • [Presentation] MONAA: a Tool for Timed Pattern Matching with Automata-Based Acceleration2018

    • Author(s)
      Masaki Waga
    • Organizer
      3rd Workshop on Monitoring and Testing of Cyber-physical Systems
    • Related Report
      2018 Annual Research Report
    • Int'l Joint Research
  • [Remarks] Masaki Waga(和賀 正樹)

    • URL

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

    • Related Report
      2020 Annual Research Report
  • [Remarks] Masaki Waga (和賀 正樹)

    • URL

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

    • Related Report
      2019 Annual Research Report
  • [Remarks] 申請者個人ウェブページ

    • URL

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

    • Related Report
      2018 Annual Research Report
  • [Patent(Industrial Property Rights)] モニタリング装置及びモニタリング方法2020

    • Inventor(s)
      和賀 正樹、エティエンヌ アンドレ、蓮尾 一郎
    • Industrial Property Rights Holder
      和賀 正樹、エティエンヌ アンドレ、蓮尾 一郎
    • Industrial Property Rights Type
      特許
    • Industrial Property Number
      2020-215603
    • Filing Date
      2020
    • Related Report
      2020 Annual Research Report
  • [Patent(Industrial Property Rights)] オートマトン生成装置、オートマトン生成方法及びプログラム2020

    • Inventor(s)
      和賀 正樹
    • Industrial Property Rights Holder
      和賀 正樹
    • Industrial Property Rights Type
      特許
    • Industrial Property Number
      2020-072577
    • Filing Date
      2020
    • Related Report
      2020 Annual Research Report
  • [Patent(Industrial Property Rights)] 情報処理装置、情報処理システム及び情報処理方法2018

    • Inventor(s)
      和賀 正樹、蓮尾 一郎
    • Industrial Property Rights Holder
      和賀 正樹、蓮尾 一郎
    • Industrial Property Rights Type
      特許
    • Filing Date
      2018
    • Related Report
      2018 Annual Research Report

URL: 

Published: 2018-05-01   Modified: 2024-03-26  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi