论文标题
限制混合系统伪造中的反例:基于惩罚的方法
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.