Constraining Counterexamples in Hybrid System Falsification: Penalty-Based Approaches
Constraining Counterexamples in Hybrid System Falsification: Penalty-Based Approaches
复制标题
DOI：
10.1007/978-3-030-55754-6_24
复制
发表时间：
2020-01
期刊：
影响因子：
--
通讯作者：
Zhenya Zhang;Paolo Arcaini;I. Hasuo
中科院分区：
文献类型：
--
作者：
Zhenya Zhang;Paolo Arcaini;I. Hasuo
混合系统的证伪作为穷举形式验证的一种实用替代方法，在信息物理系统（CPS）的质量保证中引起了越来越多的关注。在证伪中，人们寻找一个证伪输入，它驱动一个给定的黑盒模型输出一个不希望的信号。在本文中，我们确定输入约束，如约束“油门和刹车踏板不应同时按下”的汽车动力系统模型作为一个关键因素的证伪方法的实用价值。我们提出了三种方法，系统地解决输入约束优化为基础的证伪，其中两个来自字典法的约束多目标优化的背景下研究。实验证明了该方法的有效性。
Falsificationof hybrid systems is attracting ever-growing attention in quality assurance of Cyber-Physical Systems (CPS) as a practical alternative to exhaustive formal verification. In falsification, one searches for a falsifying input that drives a given black-box model to output an undesired signal. In this paper, we identifyinput constraints—such as the constraint “the throttle and brake pedals should not be pressed simultaneously” for an automotive powertrain model—as a key factor for the practical value of falsification methods. We propose three approaches for systematically addressing input constraints in optimization-based falsification, two among which come from the lexicographic method studied in the context of constrained multi-objective optimization. Our experiments show the approaches’ effectiveness.