Formal verification of unreliable failure detectors in partially synchronous systems

M. Atif, M.R. Mousavi, A.A.H. Osaiweran

Research output: Book/ReportReportAcademic

56 Downloads (Pure)

Abstract

In this paper, 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 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.
Original languageEnglish
Place of PublicationEindhoven
PublisherTechnische Universiteit Eindhoven
Number of pages21
Publication statusPublished - 2011

Publication series

NameComputer science reports
Volume1112
ISSN (Print)0926-4515

Fingerprint

Detectors
Model checking
Formal verification

Cite this

Atif, M., Mousavi, M. R., & Osaiweran, A. A. H. (2011). Formal verification of unreliable failure detectors in partially synchronous systems. (Computer science reports; Vol. 1112). Eindhoven: Technische Universiteit Eindhoven.
Atif, M. ; Mousavi, M.R. ; Osaiweran, A.A.H. / Formal verification of unreliable failure detectors in partially synchronous systems. Eindhoven : Technische Universiteit Eindhoven, 2011. 21 p. (Computer science reports).
@book{252c309223184beea35fe361fa6fdfd2,
title = "Formal verification of unreliable failure detectors in partially synchronous systems",
abstract = "In this paper, we formally verify four algorithms proposed in [M. Larrea, S. Ar{\'e}valo and A. Fern{\'a}ndez, 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.",
author = "M. Atif and M.R. Mousavi and A.A.H. Osaiweran",
year = "2011",
language = "English",
series = "Computer science reports",
publisher = "Technische Universiteit Eindhoven",

}

Atif, M, Mousavi, MR & Osaiweran, AAH 2011, Formal verification of unreliable failure detectors in partially synchronous systems. Computer science reports, vol. 1112, Technische Universiteit Eindhoven, Eindhoven.

Formal verification of unreliable failure detectors in partially synchronous systems. / Atif, M.; Mousavi, M.R.; Osaiweran, A.A.H.

Eindhoven : Technische Universiteit Eindhoven, 2011. 21 p. (Computer science reports; Vol. 1112).

Research output: Book/ReportReportAcademic

TY - BOOK

T1 - Formal verification of unreliable failure detectors in partially synchronous systems

AU - Atif, M.

AU - Mousavi, M.R.

AU - Osaiweran, A.A.H.

PY - 2011

Y1 - 2011

N2 - In this paper, 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 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.

AB - In this paper, 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 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.

M3 - Report

T3 - Computer science reports

BT - Formal verification of unreliable failure detectors in partially synchronous systems

PB - Technische Universiteit Eindhoven

CY - Eindhoven

ER -

Atif M, Mousavi MR, Osaiweran AAH. Formal verification of unreliable failure detectors in partially synchronous systems. Eindhoven: Technische Universiteit Eindhoven, 2011. 21 p. (Computer science reports).