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

Étienne André, Laurent Fribourg, Jean-Marc Mota +1

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…