Sciweavers

Share
ICFEM
2009
Springer

Role-Based Symmetry Reduction of Fault-Tolerant Distributed Protocols with Language Support

9 years 1 months ago
Role-Based Symmetry Reduction of Fault-Tolerant Distributed Protocols with Language Support
Fault-tolerant (FT) distributed protocols (such as group membership, consensus, etc.) represent fundamental building blocks for many practical systems, e.g., the Google File System. Not only does one desire rigor in the protocol design but especially in its verification given the complexity and fallibility of manual proofs. The application of model checking (MC) for protocol verification is attractive with its full automation and rich property language. However, being an exhaustive exploration method, its scalable use is very much constrained by the overall number of different system states. We observe that, although FT distributed protocols usually display a very high degree of symmetry which stems from permuting different processes, MC efforts targeting their automated verification often disregard this symmetry. Therefore, we propose to leverage the framework of symmetry reduction and improve on existing applications of it by specifying so called role-based symmetries. Our seco...
Péter Bokor, Marco Serafini, Neeraj Suri, H
Added 26 May 2010
Updated 26 May 2010
Type Conference
Year 2009
Where ICFEM
Authors Péter Bokor, Marco Serafini, Neeraj Suri, Helmut Veith
Comments (0)
books