MPI-INF Logo
Publications

Server    domino.mpi-inf.mpg.de

Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop

Author, Editor
Author(s):
Lu, Tianxiang
Merz, Stephan
Weidenbach, Christoph
dblp
dblp
dblp
Not MPG Author(s):
Merz, Stephan
Editor(s):
Bendisposto, Jens
Leuschel, Michael
Roggenbach, Markus
dblp
dblp
dblp
Not MPII Editor(s):
Bendisposto, Jens
Leuschel, Michael
Roggenbach, Markus
BibTeX cite key*:
LuTX2009
Title, Booktitle
Title*:
Model Checking the Pastry Routing Protocol
mcpastry-lu-avocs2010.pdf (98.26 KB)
Booktitle*:
10th International Workshop Automatic Verification of Critical Systems (AVOCS 2010)
Event, URLs
Conference URL::
http://www.formal-methods.de/avocs2010
Downloading URL:
Event Address*:
Düsseldorf, Germany
Language:
English
Event Date*
(no longer used):
Organization:
Microsoft Research
Event Start Date:
20 September 2010
Event End Date:
23 September 2010
Publisher
Name*:
Universität Düsseldorf
URL:
Address*:
Düsseldorf
Type:
Vol, No, Year, pp.
Series:
Volume:
Number:
Month:
September
Pages:
19-21
Year*:
2010
VG Wort Pages:
ISBN/ISSN:
Sequence Number:
DOI:
Note, Abstract, ©
(LaTeX) Abstract:
Pastry is an algorithm for implementing a scalable distributed hash table over an underlying P2P network, an active area of research in distributed systems.
Several implementations of Pastry are available and have been applied in practice, but no attempt has so far been made to formally describe the algorithm or to verify its properties. Since Pastry combines rather complex data structures, asynchronous communication, concurrency, resilience to \emph{churn} and fault tolerance, it makes an interesting target for verification. We have modeled Pastry's core routing algorithms in the specification language \texorpdfstring{\textrm{\upshape TLA\textsuperscript{+}}}{TLA+} and used its model checker \textsc{tlc} to analyze qualitative properties of Pastry such as \emph{correctness} and \emph{consistency}.
Keywords:
Model checking, Specification, Verification of software
Download
Access Level:
Public

Correlation
MPG Unit:
Max-Planck-Institut für Informatik
MPG Subunit:
Automation of Logic
Appearance:
MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, VG Wort



BibTeX Entry:

@INPROCEEDINGS{LuTX2009,
AUTHOR = {Lu, Tianxiang and Merz, Stephan and Weidenbach, Christoph},
EDITOR = {Bendisposto, Jens and Leuschel, Michael and Roggenbach, Markus},
TITLE = {Model Checking the {Pastry} Routing Protocol},
BOOKTITLE = {10th International Workshop Automatic Verification of Critical Systems (AVOCS 2010)},
PUBLISHER = {Universität Düsseldorf},
YEAR = {2010},
ORGANIZATION = {Microsoft Research},
PAGES = {19--21},
ADDRESS = {D{\"u}sseldorf, Germany},
MONTH = {September},
}


Entry last modified by Manuel Lamotte-Schubert, 03/16/2011
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
[Library]
Created
12/02/2010 10:23:47 AM
Revisions
5.
4.
3.
2.
1.
Editor(s)
Manuel Lamotte-Schubert
Manuel Lamotte-Schubert
Anja Becker
Tian Xiang Lu
Tian Xiang Lu
Edit Dates
16.03.2011 15:20:50
16.03.2011 15:20:28
07.02.2011 12:27:20
12/02/2010 10:26:36 AM
12/02/2010 10:25:15 AM


File Attachment Icon
mcpastry-lu-avocs2010.pdf