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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Property-Agnostic Base Case Extension for Scalable Verification of Distributed Systems

  • Kyle Storey,
  • Eric Mercer

摘要

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.