Preach is an industrial strength distributed explicit state model checker based on Murphi. The goal of this project was to develop a reliable, easy to maintain, scalable model checker that was compatible with the Murphi specification language. Preach is implemented in the concurrent functional language Erlang, chosen for its parallel programming elegance. We use the original Murphi front-end to parse the model description, a layer written in Erlang to handle the communication aspects of the algorithm, and also use Murphi as a back-end for state expansion and to store the hash table. This allowed a clean and simple implementation, with the core parallel algorithms written in under 1000 lines of code. This paper describes the Preach implementation including the various features that are necessary for the large models we target. We have used Preach to model check an industrial cache coherence protocol with approximately 30 billion states. To our knowledge, this is the largest number published for a distributed explicit state model checker. Preach has been released to the public under an open source BSD license.
There is a README file which explains how to run PReach. If someone has not used Murphi before, then the User Manual would be a good place to start.
Here is our presentation of PReach for details about its implementation:
Here is our paper from PDMC:
Here is the PDMC talk:
Here is a course on protocols on the web that looks good for a beginner: