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

2020 Fiscal Year Annual Research Report

• Project/Area Number: 19J15218
• Research Institution: The Graduate University for Advanced Studies
• Principal Investigator: ZHANG Zhenya 総合研究大学院大学, 複合科学研究科, 特別研究員(DC2)
• Project Period (FY): 2019-04-25 – 2021-03-31
• Keywords: falsification, / input constraints, / hierarchical framework

Outline of Annual Research Achievements

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.

Research Progress Status

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

Strategy for Future Research Activity

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

Research Products

• [Journal Article] Constraining Counterexamples in Hybrid System Falsification: Penalty-Based Approaches (2020)
  • Author(s): Zhang Zhenya、Arcaini Paolo、Hasuo Ichiro
  • Journal Title: NASA Formal Methods. NFM 2020. Volume: 12229 Pages: 401～419
  • DOI: 10.1007/978-3-030-55754-6_24
  • Peer Reviewed / Open Access / Int'l Joint Research
• [Journal Article] Hybrid System Falsification Under (In)equality Constraints via Search Space Transformation (2020)
  • Author(s): Zhang Zhenya、Arcaini Paolo、Hasuo Ichiro
  • Journal Title: IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems Volume: 39 Pages: 3674～3685
  • DOI: 10.1109/TCAD.2020.3013073
  • Peer Reviewed / Open Access / Int'l Joint Research
• [Journal Article] ARCH-COMP 2020 Category Report: Falsification (2020)
  • Author(s): 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
  • Journal Title: 7th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH20) Volume: 74 Pages: 140～152
  • DOI: 10.29007/trr1
  • Open Access / Int'l Joint Research
• [Presentation] Multi-Armed Bandits for Boolean Connectives in Hybrid System Falsification (2020)
  • Author(s): Zhenya Zhang
  • Organizer: 日本ソフトウェア科学会第 37 回大会
• [Presentation] Hybrid System Falsification Under (In)equality Constraints via Search Space Transformation (2020)
  • Author(s): Zhenya Zhang
  • Organizer: International Conference on Embedded Software (EMSOFT 2020)
  • Int'l Joint Research
• [Presentation] Constraining Counterexamples in Hybrid System Falsification: Penalty-Based Approaches (2020)
  • Author(s): Zhenya Zhang
  • Organizer: 12th NASA Formal Methods Symposium NFM 2020
  • Int'l Joint Research