Hybrid Safety Verification for Autonomous Vehicles: Integrating CTL Model Checking with Continuous Safety Scoring

When evaluating new algorithms for automated driving systems, human-comprehensibility is essential for comparative assessment. This enable researchers to benchmark iterative implementations against themselves and competing approaches across key metrics such as safety, efficiency, effectiveness, and performance. Simply comprehensible assessment is crucial in automated driving where researchers from many different fields bring their expertise. Traditionally, tests are conducted with a binary verification approach. When conducting multiple validations, a formal model checking method such as a Computational Tree Logic (CTL) can be used. Such a method can verify the safety properties of a system but provides no input regarding the degree of success or the degree of failure. Such an information would be vital when considering an iteratively updating system. This work proposes a quantitative grading system called the safety score that provides a human-comprehensible score for automated driving tests based on safety standards. The score can be viewed as a simple normalized score or a continuous grade in a known academic scale for intuitive human comprehension. This allows for the score to be easily used and interpreted in the field of automated driving where researchers from many fields work together for functional and system validation. The score is implemented as an extension to the CTL model to provide a hybrid model checking approach. This hybrid approach enables stakeholders to assess both absolute safety guarantees through CTL verification (pass/fail) and relative performance quality through quantitative safety grades. This combination supports comparative analysis between systems, facilitates regulatory communication, and provides actionable feedback for iterative development. The hybrid model has been validated in both simulation and real-world scenarios on an automated research vehicle, demonstrating its capability to detect safety violations, quantify behavioral metrics, and provide actionable feedback via the open-source Eclipse ADORe (Automated Driving Open Research) framework.

Keywords: Autonomous vehicles, formal verification, model checking, runtime verification, safety scoring, safety assessment, ROS2, CTL, temporal logic.