Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop


Show entries of:

this year (2019) | last year (2018) | two years ago (2017) | Notes URL

Action:

login to update

Options:




Library Locked Library locked




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

URL of the conference:

http://www.formal-methods.de/avocs2010

URL for downloading the paper:


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
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
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
Show details for Attachment SectionAttachment Section
Hide details for Attachment SectionAttachment Section

View attachments here:


File Attachment Icon
mcpastry-lu-avocs2010.pdf