Integrating Formal Verification and Simulation-based Assertion Checking in a Corroborative V&V Process

TL;DR

This paper proposes a framework combining formal verification, simulation-based assertion checking, and real-world testing to improve validation of autonomous vehicle safety and reliability.

Contribution

It introduces the Corroborative V&V framework integrating multiple verification levels and formal relationships to enhance AV validation confidence.

Findings

Defines a multi-level V&V process for AVs

Establishes formal relationships between verification methods

Enhances assurance confidence through corroboration

Abstract

Automated Vehicles (AVs) are rapidly maturing in the transportation domain. However, the complexity of the AV design problem is such that no single technique is sufficient to provide adequate validation of key properties such as safety, reliability or trustworthiness. In this vision paper, a combination of a spatial traffic logic and agent-based verification methods with a validation method that uses assertion checking of simulations is proposed. We sketch how to integrate the respective approaches within a methodological framework called Corroborative Verification and Validation (V&V).The Corroborative V&V framework identifies three different verification and validation levels for AVs (formal verification, simulation-based testing, real-world experiments) and specifies connections and evidence between these levels. We define specifications for the formal relationships that must be established between processes, system models and requirements models for the evidence from formal design verification and simulation-based testing to corroborate each other and enhance assurance confidence from verification and validation.