M. Atif, M.R. Mousavi and A. Osaiweran. Proceedings of the 27th ACM Symposium on Applied Computing, Dependable and Adaptive Distributed Systems (ACM SAC - DADS), Riva del Garda, Italy, ACM Press, 2012.
In this paper, we formally verify four algorithms proposed in [M. Larrea, S. Arevalo and A. Fernandez, Efficient Algorithms to Implement Unreliable Failure Detectors in Partially Synchronous Systems, 1999]. Each algorithm is specified formally as a network of timed automata and is verified with respect to completeness and accuracy properties. Using the model-checking tool UPPAAL, 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. We propose one solution for deadlock avoidance. Moreover, we use one of the algorithms studied in this paper as a measure to compare the effectiveness of three model-checking tools, namely, UPPAAL, mCRL2 and FDR2. We also show that all algorithms satisfy their completeness and accuracy properties if the required number of processes remain operational.
An extended version of this paper appeared as Technical Report CSR-11-12, TU/Eindhoven.
(Paper in .pdf format) (Presentation in .pdf format)
Bibtex Entry:
@inProceedings{MousaviSAC2012,
author = "Atif, Muhammad and Mousavi, Mohammad Reza and Osaiweran, Ammar",
title = "Formal Verification of Unreliable Failure Detectors in Partially Synchronous Systems",
booktitle = "Proceedings of the 27th ACM Symposium on Applied Computing",
publisher = "ACM Press",
year = "2012"
}