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

结合形式化方法和启发式方法，有效保证物理信息系统的质量

• 批准号: 19J15218
• 负责人: ZHANG Zhenya
• 金额: $ 1.09万
• 依托单位: The Graduate University for Advanced Studies
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for JSPS Fellows
• 财政年份: 2019
• 资助国家: 日本
• 起止时间: 2019-04-25 至 2021-03-31
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-19J15218/
• 关键词: falsification,; input constraints,; hierarchical framework; Falsification; Signal Temporal Logic; Stochastic Optimization; Quality Assurance; Cyber-Physical Systems; Search-based Testing

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.

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

项目成果

ARCH-COMP 2019 Category Report: Falsification

• DOI: 10.29007/68dk
• 发表时间: 2019
• 作者: G. Ernst;Paolo Arcaini;Alexandre Donzé;Georgios Fainekos;L. Mathesen;Giulia Pedrielli;Shakiba Yaghoubi;Yoriyuki Yamagata;Zhenya Zhang

Constraining Counterexamples in Hybrid System Falsification: Penalty-Based Approaches

• DOI: 10.1007/978-3-030-55754-6_24
• 发表时间: 2020-01
• 期刊: ArXiv
• 作者: Zhenya Zhang;Paolo Arcaini;I. Hasuo

Fast Falsification of Hybrid Systems Using Probabilistically Adaptive Input

使用概率自适应输入的混合系统的快速证伪

• DOI: 10.1007/978-3-030-30281-8_10
• 发表时间: 2019
• 期刊: Quantitative Evaluation of Systems
• 作者: Gidon Ernst;Sean Sedwards;Zhenya Zhang;Ichiro Hasuo
• 通讯作者: Ichiro Hasuo

ARCH-COMP 2020 Category Report: Falsification

ARCH-COMP 2020 类别报告：造假

• DOI: 10.29007/trr1
• 发表时间: 2020
• 期刊: 7th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH20)
• 作者: 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
• 通讯作者: Zhang Zhenya

Hybrid System Falsification Under (In)equality Constraints via Search Space Transformation

通过搜索空间变换在（不）等式约束下进行混合系统证伪

• DOI: 10.1109/tcad.2020.3013073
• 发表时间: 2020
• 期刊: IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
• 影响因子: 2.9
• 作者: Zhang Zhenya;Arcaini Paolo;Hasuo Ichiro
• 通讯作者: Hasuo Ichiro