Many distributed systems require temporal properties to hold for correctness. Model checking can verify these properties on a small system but it doesn’t scale for arbitrarily large systems. This work presents a new method for proving that temporal properties verified on a small system extend to an arbitrarily large system when that system has a ring topology.
It uses a model checker to prove temporal properties and properties of a partial order of events in the system. It then admits the partial order properties as axioms in a theorem prover and proves a conformance relation between an arbitrary-sized ring of nodes and the model-checked base case. The conformance relation is used to prove that adding a new node to the ring does not affect the possible states of the existing nodes in the system and therefore any properties proven in the small system continue to hold in an arbitrarily large system.

We demonstrate the approach in a case study of a nontrivial distributed protocol that is used by the MyCHIP’s digital currency to clear credit.