# Correct-by-Construction Advanced Driver Assistance Systems based on a Cognitive Architecture

## TL;DR

This paper introduces a formal verification approach for advanced driver assistance systems using a cognitive architecture, enabling safe, correct-by-construction system design for complex highway driving scenarios.

## Contribution

It integrates ACT-R cognitive modeling with formal methods and abstraction techniques to verify ADAS in multi-lane highway scenarios.

## Key findings

- Successful application to multi-lane highway scenarios
- Effective abstraction of continuous systems into Markov processes
- Demonstrated safety and correctness in case studies

## Abstract

Research into safety in autonomous and semi-autonomous vehicles has, so far, largely been focused on testing and validation through simulation. Due to the fact that failure of these autonomous systems is potentially life-endangering, formal methods arise as a complementary approach. This paper studies the application of formal methods to the verification of a human driver model built using the cognitive architecture ACT-R, and to the design of correct-by-construction Advanced Driver Assistance Systems (ADAS). The novelty lies in the integration of ACT-R in the formal analysis and an abstraction technique that enables finite representation of a large dimensional, continuous system in the form of a Markov process. The situation considered is a multi-lane highway driving scenario and the interactions that arise. The efficacy of the method is illustrated in two case studies with various driving conditions.