# Magnifier: A Compositional Analysis Approach for Autonomous Traffic Control

## TL;DR

Magnifier is a compositional, iterative verification approach for autonomous traffic control systems that efficiently ensures correctness at runtime by focusing on affected components and propagating changes as needed.

## Contribution

It introduces Magnifier, a novel incremental verification method that operates on component models to improve runtime verification efficiency in autonomous traffic systems.

## Key findings

- Reduces verification time compared to non-compositional methods.
- Lowers memory consumption during runtime verification.
- Effectively handles dynamic changes in traffic control components.

## Abstract

Autonomous traffic control systems are large-scale systems with critical goals. Due to the dynamic nature of the surrounding world of these systems, assuring the satisfaction of their properties at runtime and in the presence of a change is important. A prominent approach to assure the correct behavior of these systems is verification at runtime, which has strict time and memory limitations. To tackle these limitations, we propose Magnifier, an iterative, incremental, and compositional verification approach that operates on a component-based model. The Magnifier idea is zooming on the component affected by a change, verifying the correctness of properties of interest of the system after adapting the component to the change, and then zooming out and tracing the change if it propagates. If the change propagates, all components affected by the change are adapted and are composed to form a new component. Magnifier repeats the same process for the new component. This iterative process terminates whenever the propagation of the change stops. In Magnifier, we use the Coordinated Adaptive Actor model (CoodAA) of traffic control systems. We present a formal semantics for CoodAA as a network of Timed Input-Output Automata (TIOAs). The change does not propagate if TIOAs of the adapted component and its environment are compatible. We implement our approach in Ptolemy II. The results of our experiments indicate that the proposed approach improves the verification time and the memory consumption compared to a non-compositional approach.