Certification of an exact worst-case self-stabilization time

Unlike qualitative properties such as correctness (safety and liveness), quantitative proper-ties of distributed algorithms have only been certified in very few studies. This work is the first attempt to certify time complexity bounds of a fault-tolerant distributed algorithm. Our case study consists in formally proving, using the Coq proof assistant, the time complexity of the first Dijkstra's self-stabilizing token ring algorithm. In more detail, we formally prove both the self-stabilization and exact worst-case stabilization time of this algorithm assuming asynchronous settings. This latter result is obtained in two main steps. First, we certify a non-trivial upper bound on the stabilization time, i.e., every execution in an N-size ring contains at most 3middotNmiddot(N-1) 2 - N -1 steps if N > 4, at most 3 steps if N = 3; and in remaining cases, the stabilization time is zero. Then, for each case, we exhibit a possible execution whose complexity exactly matches those upper bounds. Notice that the tight bounds for N = 3 and N > 4 were unknown until now, even among self-stabilization researchers.(c) 2022 Elsevier B.V. All rights reserved.