uu.seUppsala University Publications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Testing And Verifying Chain Repair Methods For CORFU Using Stateless Model Checking
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science. (Programming Languages)
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science. (Programming Languages)ORCID iD: 0000-0001-9657-0179
VMware, Cambridge, MA, USA.
2017 (English)Conference paper, Published paper (Refereed)
Abstract [en]

Corfu is a distributed shared log that is designed to be scalable and reliable in the presence of failures and asynchrony. Internally, Corfu is fully replicated for fault tolerance, without sharding data or sacrificing strong consistency. In this case study, we present the modeling approaches we followed to test and verify, using Concuerror, the correctness of repair methods for the Chain Replication protocol suitable for Corfu. In the first two methods we tried, Concuerror located bugs quite fast. In contrast, the tool did not manage to find bugs in the third method, but the time this took also motivated an improvement in the tool that reduces the number of traces explored. Besides more details about all the above, we present experiences and lessons learned from applying stateless model checking for verifying complex protocols suitable for distributed programming.

Place, publisher, year, edition, pages
Cham: Springer, 2017. 227-242 p.
Series
Lecture Notes in Computer Science, 10510
National Category
Computer Systems Software Engineering
Identifiers
URN: urn:nbn:se:uu:diva-331836DOI: 10.1007/978-3-319-66845-1_15ISBN: 978-3-319-66844-4 (print)ISBN: 978-3-319-66845-1 (electronic)OAI: oai:DiVA.org:uu-331836DiVA: diva2:1150359
Conference
Integrated Formal Methods. IFM 2017
Projects
UPMARC
Available from: 2017-10-18 Created: 2017-10-18 Last updated: 2017-11-22Bibliographically approved
In thesis
1.
The record could not be found. The reason may be that the record is no longer available or you may have typed in a wrong id in the address field.

Open Access in DiVA

fulltext(196 kB)10 downloads
File information
File name FULLTEXT01.pdfFile size 196 kBChecksum SHA-512
a5b64858c16fdaae5659d60483d44206010edf293cba4f2cd7beb7a5d3d1b60d22774eee49f35ea601bd3696a2d5ae240a98e75540534b33b52b6ce020d82683
Type fulltextMimetype application/pdf

Other links

Publisher's full text

Authority records BETA

Aronis, StavrosSagonas, Konstantinos

Search in DiVA

By author/editor
Aronis, StavrosSagonas, Konstantinos
By organisation
Computing Science
Computer SystemsSoftware Engineering

Search outside of DiVA

GoogleGoogle Scholar
Total: 10 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 32 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf