Skip to Main content Skip to Navigation
Reports

Guard Automata for the Verification of Safety and Liveness of Distributed Algorithms (long version)

Nathalie Bertrand 1 Bastien Thomas 1 Josef Widder 2 
1 SUMO - SUpervision of large MOdular and distributed systems
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : Distributed algorithms typically run over arbitrary many processes and may involve unboundedly many rounds, making the automated verification of their correctness challenging. Building on domain theory, we introduce a framework that abstracts infinite-state distributed systems that represent distributed algorithms into finite-state guard automata. The soundness of the approach corresponds to the Scott-continuity of the abstraction, which relies on the assumption that the distributed algorithms are layered. Guard automata thus enable the verification of safety and liveness properties of distributed algorithms.
Document type :
Reports
Complete list of metadata

https://hal.inria.fr/hal-03283388
Contributor : Nathalie Bertrand Connect in order to contact the contributor
Submitted on : Saturday, July 10, 2021 - 9:30:01 AM
Last modification on : Monday, April 4, 2022 - 9:28:24 AM
Long-term archiving on: : Monday, October 11, 2021 - 6:04:25 PM

File

hal-version.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-03283388, version 1

Citation

Nathalie Bertrand, Bastien Thomas, Josef Widder. Guard Automata for the Verification of Safety and Liveness of Distributed Algorithms (long version). [Technical Report] Inria. 2021, pp.1-33. ⟨hal-03283388⟩

Share

Metrics

Record views

27

Files downloads

80