A few fault-tolerant distributed algorithms encoded in parametric Promela. The modeling decisions are illustrated in our Spin'13 paper, where we checked the benchmarks with Spin:
Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder.
Towards Modeling and Model Checking Fault-Tolerant Distributed Algorithms.
SPIN, volume 7976 of LNCS, pages 209-226, 2013.
A more detailed exposition can be found in the SFM'14 tutorial. A recent overview of the techniques is available at PSI'15.
After SPIN'13 we collected new benchmarks and extended them for parameterized
model checking with NuSMV and
FAST. The benchmarks are using
symbolic expressions like assume(...) that cannot be directly translated
into standard Promela. We used the
benchmarks to evaluate the techniques presented at
SPIN'13,
FMCAD'13,
CONCUR'14,
CAV'15,
POPL'17,
and FMSD'17.
Feel free to use the benchmarks, as long as you are citing us :-)
You can generate standard (non-parameterized) Promela code using our tool ByMC
Directory spin13 contains both parameterized benchmarks and fixed-size benchmarks in standard Promela.
If you have any questions about the benchmarks, ask Igor Konnov