Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1145/2245276.2245369 | Linear Algebra and its Applications |
Keywords | Field | DocType |
accuracy property,m. larrea,partially synchronous systems,large buffer,implement unreliable failure detectors,non-faulty node,communication channel,model-checking tool,s. ar,efficient algorithms,formal verification,model checking,computer and information science,distributed algorithms | Model checking,Parallel algorithm,Computer science,Parallel computing,Automaton,Deadlock,Distributed algorithm,Arbitrarily large,Formal verification,Buffer overflow | Conference |
Citations | PageRank | References |
1 | 0.40 | 10 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| M. Atif | 1 | 1 | 0.40 |
| M. R. Mousavi | 2 | 220 | 11.42 |
| aah osaiweran | 3 | 1 | 0.40 |