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

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

• 批准号: 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

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

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

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