混杂系统证伪中的约束反例:基于惩罚的方法
Constraining Counterexamples in Hybrid System Falsification: Penalty-Based Approaches
摘要:
混杂系统的证伪作为穷举形式化验证的一种实用替代方法,在信息物理系统(CPS)的质量保证中引起了越来越多的关注。在证伪中,人们寻找一个证伪输入,它驱动一个给定的黑盒模型输出一个不希望的信号。在本文中,我们确定输入约束-如约束“油门和刹车踏板不应同时按下”的汽车动力系统模型-作为一个关键因素的证伪方法的实用价值。我们提出了三种方法,系统地解决输入约束优化为基础的证伪,其中两个来自字典法的约束多目标优化的背景下研究。实验证明了该方法的有效性。
英文摘要:
Falsification of 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 identify input constraints---such as the constraint "the throttle and brake pedals should not 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.
机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。