| 研究開始時の研究の概要 |
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.
|
| 研究実績の概要 |
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.
|
