# Verification of an industrial asynchronous leader election algorithm using abstractions and parametric model checking

## TL;DR

This paper verifies the correctness of an industrial asynchronous leader election algorithm capable of handling many processes and failures using abstraction and parametric model checking.

## Contribution

It introduces a novel verification approach combining abstraction, SafeProver, and parametric timed model checking for large-scale industrial algorithms.

## Key findings

- Proved correctness for up to 5000 processes
- Validated the algorithm's robustness against failures
- Demonstrated scalability of the verification method

## Abstract

The election of a leader in a network is a challenging task, especially when the processes are asynchronous, i.e., execute an algorithm with time-varying periods. Thales developed an industrial election algorithm with an arbitrary number of processes, that can possibly fail. In this work, we prove the correctness of a variant of this industrial algorithm. We use a method combining abstraction, the SafeProver solver, and a parametric timed model-checker. This allows us to prove the correctness of the algorithm for a large number p of processes (p=5000).

---
Source: https://tomesphere.com/paper/1812.08949