形式手法とヒューリスティクスの組み合わせによる物理情報システムの効率的な品質保証
| Project/Area Number |
19J15218
|
|---|
| Research Category |
Grant-in-Aid for JSPS Fellows
|
| Allocation Type | Single-year Grants |
|---|
| Section | 国内 |
|---|
| Review Section |
Basic Section 60050:Software-related
|
|---|
| Research Institution | The Graduate University for Advanced Studies |
|---|
Principal Investigator |
ZHANG Zhenya 総合研究大学院大学, 複合科学研究科, 特別研究員(DC2)
|
|---|
| Project Period (FY) |
2019-04-25 – 2021-03-31
|
| Project Status |
Completed (Fiscal Year 2020)
|
| Budget Amount *help |
¥1,700,000 (Direct Cost: ¥1,700,000)
Fiscal Year 2020: ¥800,000 (Direct Cost: ¥800,000)
Fiscal Year 2019: ¥900,000 (Direct Cost: ¥900,000)
|
|---|
| Keywords | falsification, / input constraints, / hierarchical framework / Falsification / Signal Temporal Logic / Stochastic Optimization / Quality Assurance / Cyber-Physical Systems / Search-based Testing |
|---|
| Outline of Research at the Start |
Cyber-Physical Systems (CPS) nowadays are permeating people’s daily life. The safety-criticality of CPS poses challenges in quality assurance. While verification is infeasible due to the infinite state space, testing techniques which aim at a counterexample to refute the system specification are pursued. My research topic, namely falsification, solves the system testing problem through stochastic optimization. Different backend techniques, including formal methods, metaheuristics, AI, etc., collaborate in my research together for the goal of high-quality, safety-assured CPS products.
|
| 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年度が最終年度であるため、記入しない。
|
Report
(2 results)
Research Products
(11 results)
-
-
-
[Journal Article] ARCH-COMP 2020 Category Report: Falsification2020
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
Related Report
Open Access / Int'l Joint Research
-
-
-
[Journal Article] ARCH-COMP 2019 Category Report: Falsification2019
Author(s)
Gidon Ernst, Paolo Arcaini, Alexandre Donze, Georgios Fainekos, Logan Mathesen, Giulia Pedrielli, Shakiba Yaghoubi, Yoriyuki Yamagata, Zhenya Zhang
-
Journal Title
6th International Workshop on Applied Verification of Continuous and Hybrid Systems
Volume: 61
Pages: 129-140
DOI
Related Report
Open Access / Int'l Joint Research
-
-
-
-
-
