English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Consensus protocols are widely used in building reliable distributed softwaresystems and its correctness is of vital importance. TLA+ is a lightweightformal specification language which enables precise specification of systemdesign and exhaustive checking of the design without any human effort. Thefeatures of TLA+ make it widely used in the specification and model checking ofconsensus protocols, both in academia and industry. However, the application ofTLA+ is limited by the state explosion problem in model checking. Thoughcompositional model checking is essential to tame the state explosion problem,existing compositional checking techniques do not sufficiently consider thecharacteristics of TLA+.  In this work, we propose the Interaction-Preserving Abstraction (IPA)framework, which leverages the features of TLA+ and enables practical andefficient compositional model checking of consensus protocols specified inTLA+. In the IPA framework, system specification is partitioned into multiplemodules, and each module is divided to the internal part and the interactionpart. The basic idea of the interaction-preserving abstraction is to omit theinternal part of each module, such that another module cannot distinguishwhether it is interacting with the original module or the coarsened abstractone.  We use the IPA framework to the compositional checking of the TLA+specification of two consensus protocols Raft and ParallelRaft. Raft is aconsensus protocol which is originally developed in the academia and thenwidely used in industry. ParallelRaft is the replication protocol in PolarFS,the distributed file system for the commercial database Alibaba PoloarDB. Wedemonstrate that the IPA framework is easy to use in realistic scenarios and atthe same time significantly reduces the model checking cost.

Compositional Model Checking of Consensus Protocols Specified in TLA+ via Interaction-Preserving Abstraction