Formal verification of Unreliable Failure Detectors in Partially Synchronous Systems
Muhammad Atif, Mohammad Reza Mousavi, Ammar Osaiweran · 2012
We formally verify four algorithms proposed in [M. Larrea, S. Arévalo and A. Fernández, Efficient Algorithms to Implement Unreliable Failure Detectors in Partially Synchronous Systems, 1999]. Each algorithm is specified as a network of timed automata and is verified with respect to completeness and accuracy properties. Using the model-checking tool UP-PAAL, we detect and report the occurrences of deadlock (for all algorithms) between each pair of non-faulty nodes due to buffer overflow in communication channels with arbitrarily large buffers and we propose a solution. Moreover, we use one of the algorithms as a measure to compare three model-checking tools, namely, UPPAAL, mCRL2 and FDR2.