Specification and model checking of the Chandy and Lamport distributed snapshot algorithm in rewriting logic

Abstract

Many model checkers have been developed and then many case studies have been conducted by applying them to mechanical analysis of systems including distributed systems, protocols and algorithms. To the best of our knowledge, however, there are few case studies in which the Chandy & Lamport distributed snapshot algorithm is mechanically analyzed with model checkers. We think that this is because it is not straightforward to express the significant property that the algorithm should enjoy in LTL and CTL. In this paper, we describe how to specify the algorithm in Maude, a specification and programming language based on rewriting logic, and how to model check the significant property with the Maude search command, which demonstrates the power of the command. The case study also demonstrates the importance of case analysis in specification. © 2012 Springer-Verlag.