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

今年，在我的主管Hasuo Ichiro Hasuo和我的同事Paolo Arcaini的帮助下，我的工作顺利进行。我们的最后一项工作[NFM‘20]提出了一个问题，即经典的伪造工作流程不能处理对输入的逻辑约束，例如，“油门和刹车不能同时按下”。我们在这项工作中提出了基于惩罚的方法来解决这个问题。然而，由于引入了惩罚，优化的性能受到了损害。为了提高性能，我们提出了一种新的方法，称为搜索空间变换。其基本思想是在无约束空间和有约束输入空间之间建立映射，并根据有约束空间中的稳健性定义无约束空间中的适应度。然后我们可以在无约束空间中搜索，一旦找到反例，我们就返回输入空间中的映射点作为算法的结果。由于返回点位于输入空间，因此保证满足输入约束。我们通过实验证明了该方法的优越性。这项工作已经发表在[EMSOFT‘20]上，我也完成了我的博士论文，在其中我总结了我的博士论文。它主要包括改进现有证伪框架的不同技术。总体而言，我提出了一个层次化的证伪框架。该框架分为两层：顶层选择一个子问题进行处理；底层运行选定的子问题，并将反馈反馈给顶层以供其进一步决策。

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.