Traditional industrial testing methods often fail to guarantee that a system behaves as expected due to the resource cost of exhaustively searching for defects. To minimize this cost, a promising alternative called robustness-guided falsification is emerging as a less exhaustive method that can handle the increasing complexity of autonomous driving systems. This approach attempts to identify counterexamples to a given system property by treating testing as an optimization problem with a robustness function to be minimized. This function quantifies how well the system satisfies a given property encoded as a logical formula, with values that indicate how close the system is to violating the property. In this paper, we apply robustness-guided falsification to a particular type of spatio-temporal logic, \(LTL \times MS^{\le }\) , which integrates both temporal and spatial modalities to describe system behavior across time and space. We establish a correspondence between the Boolean semantics of the “subset or equal” relation and the degrees of robustness with signed Hausdorff distances, propose a robust semantics for \(LTL \times MS^{\le }\) , and demonstrate how robustness-guided falsification can be applied to properties expressed in this logic. To evaluate our approach, we conducted an empirical case study in a traffic scenario. The results demonstrate the feasibility of this approach in falsifying spatio-temporal properties and support the adoption of counterexample generation for the verification of defects in realistic autonomous driving systems.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Robust Spatio-Temporal Logic Semantics for Autonomous Driving Systems Falsification

  • Tiago Sequeira,
  • André Matos Pedro

摘要

Traditional industrial testing methods often fail to guarantee that a system behaves as expected due to the resource cost of exhaustively searching for defects. To minimize this cost, a promising alternative called robustness-guided falsification is emerging as a less exhaustive method that can handle the increasing complexity of autonomous driving systems. This approach attempts to identify counterexamples to a given system property by treating testing as an optimization problem with a robustness function to be minimized. This function quantifies how well the system satisfies a given property encoded as a logical formula, with values that indicate how close the system is to violating the property. In this paper, we apply robustness-guided falsification to a particular type of spatio-temporal logic, \(LTL \times MS^{\le }\) , which integrates both temporal and spatial modalities to describe system behavior across time and space. We establish a correspondence between the Boolean semantics of the “subset or equal” relation and the degrees of robustness with signed Hausdorff distances, propose a robust semantics for \(LTL \times MS^{\le }\) , and demonstrate how robustness-guided falsification can be applied to properties expressed in this logic. To evaluate our approach, we conducted an empirical case study in a traffic scenario. The results demonstrate the feasibility of this approach in falsifying spatio-temporal properties and support the adoption of counterexample generation for the verification of defects in realistic autonomous driving systems.