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

今年，在我的主管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.