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

2020 年度 実績報告書

形式手法とヒューリスティクスの組み合わせによる物理情報システムの効率的な品質保証

研究課題

研究課題/領域番号 19J15218
研究機関総合研究大学院大学

研究代表者

ZHANG Zhenya  総合研究大学院大学, 複合科学研究科, 特別研究員(DC2)

研究期間 (年度) 2019-04-25 – 2021-03-31
キーワードfalsification, / input constraints, / hierarchical framework
研究実績の概要

This year, with the help of my supervisor Ichiro Hasuo, and my colleague Paolo Arcaini, my work went on smoothly.

Our last work [NFM’20] raised a problem that the classic falsification workflow does not handle logical constraints on inputs, e.g., “the throttle and brake cannot be pushed simultaneously”. We proposed penalty-based methods in that work to solve the problem. However, due to the introduction of penalty, the performance of optimization is harmed. To improve the performance, we propose a new methodology that is called search space transformation. The basic idea is that we construct a map between an unconstrained space and the constrained input space, and we define the fitness in the unconstrained space according to the robustness in the constrained space. Then we can search in the unconstrained space, and once we find a counterexample, we return the mapped point in the input space as the result of the algorithm. Since the returned point is in the input space, it is guaranteed to satisfy the input constraint. We experimentally show the superiority of our method. This work has been published in [EMSOFT’20].

I also finished my doctoral thesis, in which I summarize my PhD works. It mainly includes different techniques that improve the existing falsification framework. Overall, I propose a hierarchical framework for falsification. The framework consists in two layers: the top layer selects a sub-problem to proceed; the bottom layer runs the selected sub-problem and returns feedback to the top layer for its further decision.

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

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

今後の研究の推進方策

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

  • 研究成果

    (6件)

すべて 2020

すべて 雑誌論文 (3件) (うち国際共著 3件、 査読あり 2件、 オープンアクセス 3件) 学会発表 (3件) (うち国際学会 2件)

  • [雑誌論文] Constraining Counterexamples in Hybrid System Falsification: Penalty-Based Approaches2020

    • 著者名/発表者名
      Zhang Zhenya、Arcaini Paolo、Hasuo Ichiro
    • 雑誌名

      NASA Formal Methods. NFM 2020.

      巻: 12229 ページ: 401~419

    • DOI

      10.1007/978-3-030-55754-6_24

    • 査読あり / オープンアクセス / 国際共著
  • [雑誌論文] Hybrid System Falsification Under (In)equality Constraints via Search Space Transformation2020

    • 著者名/発表者名
      Zhang Zhenya、Arcaini Paolo、Hasuo Ichiro
    • 雑誌名

      IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems

      巻: 39 ページ: 3674~3685

    • DOI

      10.1109/TCAD.2020.3013073

    • 査読あり / オープンアクセス / 国際共著
  • [雑誌論文] ARCH-COMP 2020 Category Report: Falsification2020

    • 著者名/発表者名
      Ernst Gidon、Arcaini Paolo、Bennani Ismail、Donze Alexandre、Fainekos Georgios、Frehse Goran、Mathesen Logan、Menghi Claudio、Pedrielli Giulia、Pouzet Marc、Yaghoubi Shakiba、Yamagata Yoriyuki、Zhang Zhenya
    • 雑誌名

      7th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH20)

      巻: 74 ページ: 140~152

    • DOI

      10.29007/trr1

    • オープンアクセス / 国際共著
  • [学会発表] Multi-Armed Bandits for Boolean Connectives in Hybrid System Falsification2020

    • 著者名/発表者名
      Zhenya Zhang
    • 学会等名
      日本ソフトウェア科学会第 37 回大会
  • [学会発表] Hybrid System Falsification Under (In)equality Constraints via Search Space Transformation2020

    • 著者名/発表者名
      Zhenya Zhang
    • 学会等名
      International Conference on Embedded Software (EMSOFT 2020)
    • 国際学会
  • [学会発表] Constraining Counterexamples in Hybrid System Falsification: Penalty-Based Approaches2020

    • 著者名/発表者名
      Zhenya Zhang
    • 学会等名
      12th NASA Formal Methods Symposium NFM 2020
    • 国際学会

URL: 

公開日: 2021-12-27  

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

Powered by NII kakenhi