We report on recent research lines related to parameterized verification and model checking applied to formal models of distributed algorithms. Both approaches are based on graph rewriting and graph transformation systems. Case-studies include distributed mutual exclusion protocols like Ricart-Agrawala, routing protocols like link reversal, and distributed consensus protocols like Paxos. Verification algorithms for restricted classes of models exploit finite-state abstractions, symbolic representations based on graph orderings, the theory of well-structured transition systems, and reachability algorithms based on labeling procedures. © 2014 Springer International Publishing Switzerland.

Parameterized verification and model checking for distributed broadcast protocols

Delzanno, Giorgio
2014

Abstract

We report on recent research lines related to parameterized verification and model checking applied to formal models of distributed algorithms. Both approaches are based on graph rewriting and graph transformation systems. Case-studies include distributed mutual exclusion protocols like Ricart-Agrawala, routing protocols like link reversal, and distributed consensus protocols like Paxos. Verification algorithms for restricted classes of models exploit finite-state abstractions, symbolic representations based on graph orderings, the theory of well-structured transition systems, and reachability algorithms based on labeling procedures. © 2014 Springer International Publishing Switzerland.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11567/893573
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 4
  • ???jsp.display-item.citation.isi??? ND
social impact