Open Challenges in the Formal Verification of Autonomous Driving

In plain words

Self-driving cars are built from many parts, such as cameras, perception software and computer chips, and each part often comes from a different company that does not show how it works inside. This makes it hard to prove that the whole car behaves safely.

The paper looks at one real project: a car that watches the driver for signs of drowsiness and combines that with sensors in a smart-city area. It points out two problems that are still open. The first is how to reason about parts that are guesses rather than certainties and whose inner workings are hidden. The second is how to place the car's software onto its computer chips so that the system stays fast and keeps working when a part fails.

The authors suggest that formal verification, a way of checking a system against written rules, could help. They sketch how contracts between parts and checks while the car runs could be combined for this purpose. This is a short position paper. It does not build or test such a system.

TL;DR

• Position paper with a case study, not a method paper; no experiments and no quantitative results §5.
• Open challenge 1: verify a system built from black-box, probabilistic components §2, §3.1.
• Open challenge 2: map software onto many-core hardware with redundancy and voting, verified formally §2, §3.2.
• Suggested tools: assume-guarantee verification, runtime verification with uncertainty, probabilistic model checking §3.1, §3.2.

Problem

Autonomous vehicles are assembled from components that come from different suppliers, and some of them are black boxes whose internals cannot be inspected §1, §2. Certification then has to rely on what each component promises rather than on its implementation §3.1. The authors name two consequences that they treat as open:

• Open Challenge 1 (composition of probabilistic modules). Perception pipelines are hierarchies of sub-components, each with a performance figure (frames per second) and a nominal accuracy. The overall accuracy of the system is not derived from these parts today §2.
• Open Challenge 2 (mapping onto computing cores). The algorithms can run on several of the cores of a multi-core, GPU or reconfigurable-hardware platform, and the mapping must be efficient and fault tolerant §2, §3.2.

The paper assumes a real-time setting for challenge 2 §3.2. It also states that formal methods have practical limits: expertise, scalability, the interpretation of results, uncertain environments and cost §4.

Method

The paper proposes no new algorithm. Its contribution is a case study, two challenges, and a set of existing techniques it suggests applying §1, §3. The suggestions are summarised below in the paper's own terms.

Challenge 1: heterogeneous composition §3.1

1. Treat the system as components with assumptions (what a component needs from the rest of the system) and guarantees (what it provides when it runs correctly). Black-box components can take part if their assumptions and guarantees are documented §3.1.
2. Use heterogeneous assume-guarantee verification to check that the components fit together. The paper relies on the approach of arXiv:2208.05507 for this §1, §3.1.
3. Add runtime verification to check, while the system runs, that each component keeps its assumptions and guarantees. Assume-guarantee alone takes these as given §3.1.
4. Because perception outputs carry uncertainty, including uncertainty about the future, plain runtime verification is not enough. The paper points to runtime verification with uncertainty as the needed technique §2, §3.1.
5. Treat machine-learning components separately, since their non-determinism needs specialised verification and hybrid testing §3.1, §4.

# Check black-box components against their contracts at runtime  [§3.1]
# Input:  components, each with assumptions and guarantees; event trace
# Output: a verdict per component and contract, per observed event

def monitor_system(components, trace):
    # Collect the assumptions and guarantees of each component  [§3.1]
    contracts = [c.assumptions + c.guarantees for c in components]
    for event in trace:
        # Check every contract on the observed event  [§3.1]
        for contract in contracts:
            verdict = evaluate(contract, event)
            # Uncertain outputs need more than true or false  [§3.1, §4]
            report(verdict)

The pseudocode restates the runtime-check idea in §3.1. The paper does not define evaluate, the verdict type, or the monitor itself; the names are ours.

Challenge 2: mapping and redundancy §3.2

1. Verify that software components are placed on cores in a way that is efficient and reliable, and that redundancy and voting are implemented correctly §3.2.
2. Use formal verification of fault-tolerant hardware designs as a starting point. The paper cites a hardware-verification study for this, and the study's full reference is in the bibliography §3.2.
3. Use probabilistic model checking of resource-management schemes for many-core systems. The paper cites the PRISM model checker and its analysis of different schemes, and suggests the same kind of analysis for mapping software to cores §3.2.

Figures and tables

• The case study is shown in four figures: the use case and vehicle architecture fig. 1, the Modena smart-area layout fig. 2, the driver-monitoring pipeline fig. 3 and the next-generation ECU architecture fig. 4 §2. The numbering follows the order in the source; check it against the compiled PDF.
• The paper has no equations, no algorithms and no tables.

Hyperparameters

The paper reports no training or model hyperparameters. The rows below are the system and platform details it does state.

Results

Author-reported. The paper is a position paper and reports no experiments, benchmarks or measured numbers §5. Setup of the case study: a research vehicle with an in-house driver-monitoring system (white box) and sensor data from a smart-city area §2.

Paper vs code

No official code.

The paper and abstract link no code. The only URLs in the source are the EPTCS template page and the footnotes to the AI4CSM project and the MASA smart-area site §2, which are project pages and not code. A GitHub repository search for the title words and for "ferrando autonomous driving verification" returned no results.

Pitfalls

• No method to implement. The contracts, the verdict logic, the mapping procedure and the probabilistic models are not specified. An implementer must design all of them. The pseudocode above is our reading of §3.1.
• Future tools are not used. The authors plan to apply the VITAMIN tool (arXiv:2403.02170) to their case study, but this is listed as future work and not done in the paper §5.
• Claims are hedged. The paper says the methods can "theoretically" enhance reliability §5. Statements such as "we can guarantee" in §3.2 describe the intent of the proposed approach, not a demonstrated result.
• Challenge 2 borrows from another domain. The fault-tolerance work it leans on targets hardware designs, and the authors say it does not come from autonomous driving §3.2.
• A third challenge was dropped. The source contains a commented-out challenge about contention on shared hardware. It is not in the paper, so do not cite it §2.
• Uncertainty is named, not solved. Runtime verification with uncertainty is described as needed, and the cited work is said to be under active research §4.
• Section numbering. The case study (§2) has no numbered subsections; its challenges appear as bold or centred paragraphs. Cite them as §2.
• Figures. Figure numbers were read from the LaTeX order because no compiled PDF was read. Confirm them before relying on a figure citation.

Lineage

• Builds on: arXiv:2208.05507 (compositional assume-guarantee verification of modular robotic systems), cited as the basis for heterogeneous verification §1, §3.1.
• Surveyed in: a survey of formal verification for autonomous systems is cited as the general overview §3.
• Future work refers to: VITAMIN, arXiv:2403.02170 §5.
• Compared against: none.
• Superseded by: not known from content in this wiki.