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.
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 normal Promela. We used the
benchmarks to evaluate the techniques presented at
SPIN'13,
FMCAD'13,
CONCUR'14,
and CAV'15.
Feel free to use the benchmarks, as long as you cite 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