| Popis: |
This paper details the design of an autonomous vehicle CAD toolchain, which captures formal descriptions of driving scenarios in order to develop a safety case for an autonomous vehicle (AV). Rather than focus on a particular component of the AV, like adaptive cruise control, the toolchain models the end-to-end dynamics of the AV in a formal way suitable for testing and verification. First, a domain-specific language capable of describing the scenarios that occur in the day-to-day operation of an AV is defined. The language allows the description and composition of traffic participants (e.g., other vehicles and traffic control devices), and the specification of formal correctness requirements. A scenario described in this language is an executable that can be processed by a specification-guided automated test generator (bug hunting), and by an exhaustive reachability tool. The toolchain allows the user to exploit and integrate the strengths of both testing and reachability, in a way not possible when each is run alone. Finally, given a particular execution of the scenario that violates the requirements, a visualization tool can display this counter-example and generate labeled sensor data. The effectiveness of the approach is demonstrated on three autonomous driving scenarios drawn from a collection of 36 scenarios that account for over 95% of accidents nationwide. These case studies demonstrate robustness-guided verification heuristics to reduce analysis time, counterexample visualization for identifying controller bugs in both the discrete decision logic and low-level analog (continuous) dynamics, and identification of modeling errors (e.g., traffic behaviors) that lead to unrealistic environment behavior. |
