一句话：结合工业仿真器与形式化测试环境，系统化生成高风险场景并用一阶线性时序逻辑在运行时监控属性。
本文研究一种严谨的、基于仿真与测试的自动驾驶系统验证方法，将现有的工业仿真器与形式化定义的测试环境集成。该环境包含驱动仿真过程的场景生成器和运行时监控器，后者检查系统被观测行为是否满足待验证的系统属性。验证方法的核心是从仿真器中抽取被仿真系统的语义模型，其中包括度量图（metric graph）——车辆所处演化环境的数学模型。监控器可验证用一阶线性时序逻辑（FO-LTL）形式化的属性，并在属性不满足时给出诊断解释。与许多仿真器采用随机探索不同，作者提出系统化生成场景集合的方法，以覆盖潜在的风险情形，尤其是必须遵守特定交通规则的不同类型路口。实验表明，对风险情境的系统化探索揭示了真实仿真器中大量缺陷，而这些缺陷很难通过随机探索被发现。
We investigate a rigorous simulation and testing-based validation method for autonomous driving systems that integrates an existing industrial simulator and a formally defined testing environment. The environment includes a scenario generator that drives the simulation process and a monitor that checks at runtime the observed behavior of the system against a set of system properties to be validated. The validation method consists in extracting from the simulator a semantic model of the simulated system including a metric graph, which is a mathematical model of the environment in which the vehicles of the system evolve. The monitor can verify properties formalized in a first-order linear temporal logic and provide diagnostics explaining their non-satisfaction. Instead of exploring the system behavior randomly as many simulators do, we propose a method to systematically generate sets of scenarios that cover potentially risky situations, especially for different types of junctions where specific traffic rules must be respected. We show that the systematic exploration of risky situations has uncovered many flaws in the real simulator that would have been very difficult to discover by a random exploration process.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@inproceedings{abs-2301-03941,
title = {Simulation-Based Validation for Autonomous Driving Systems},
author = {Changwen Li and Joseph Sifakis and Qiang Wang and Rongjie Yan and Jian Zhang},
booktitle = {ISSTA},
year = {2023},
doi = {10.1145/3597926.3598100}
}