Here you can find the benchmarks that we used in the Spin'13 paper.
The benchmarks come in two different flavours:
-
Parameterized code in parametric Promela are located in directory.
-
Non-parameterized code in standard Promela (caution: thousands of files).
Here is the short summary:
| Name | Short description | Faults | Assumptions | Specifications |
|---|---|---|---|---|
| bcast-fisman-crash | Folklore reliable broadcast, TACAS'08 | clean crashes | N > 1 | unforgeability, correctness, relay, tacas08 |
| asyn-byzagreement0 | Asynchronous Byzantine agreement | Byzantine | N > 3 * T, T >= F >= 0 | unforgeability, correctness, agreement |
| cond-consensus2 | Condition-based consensus | Byzantine | N > 2 * T, T >= F >= 0 | validity, agreement, termination |
| bcast-byz | Asynchronous reliable broadcast | Byzantine | N >= 3 * T, T >= F >= 0 | unforgeability, correctness, relay |
| bcast-clean | Asynchronous reliable broadcast | clean crashes | N > T + 1, Tc >= Fc >= Fnc >= 0 | unforgeability, correctness, relay |
| bcast-omit | Asynchronous reliable broadcast | omission | N > 2 * T, To >= Fo >= 0 | unforgeability, correctness, relay |
| bcast-symm | Asynchronous reliable broadcast | symmetric | N > 2 * T, T >= Fp >= Fs >= 0 | unforgeability, correctness, relay |
| bcast-omit-byz | Asynchronous reliable broadcast | omission + Byzantine | too long (see source) | unforgeability, correctness, relay |
| bcast-symm-byz | Asynchronous reliable broadcast | symmetric + Byzantine | too long (see source) | unforgeability, correctness, relay |
| bcast-comm-byz | Asynchronous reliable broadcast | communication + Byzantine | too long (see source) | unforgeability, correctness, relay |