|
|
|
|
||
|
The Murphi tool was originally developed by Professor David Dill's group at Stanford. It is an enumerative (explicit state) model checker, with its own input language (also called Murphi) which is a guard -> action notation similar to Unity, which are repeatedely executed in an infinite loop.
The Murphi language contains support for familiar data types for programmers (subranges, enumerated types, arrays, and records), as well as more advanced types such as the multiset, or scalarset. Murphi has a formal verifier that is based on explicit state enumeration, which can be performed as a depth-first or breadth-first search of the state space. States encountered in this mode are saved in a hash table. States generated that exist in the hash table are not expanded.
Murphi is still widely used, especially by the Microprocessor industry, to verify cache coherence protocols.
Many versions of Murphi have since been developed both by this group and others. This page contains a description of the various versions of Murphi that have been developed over the years as well as download links. The version of Murphi described herein may have slightly altered functionality than the desription above, which mainly describes the original (standard) Murphi.
Murphi has been the basis for many research projects. Descriptions and downloads for various tools are listed here.
A port to 64-bit architectures has been perfromed by this group (by Igor Mellatti). The latest version is based on CMurphi, which overcomes the hash compaction implementation of CMurphi 3.1, thus also working on 64-bit hardware. Moreover, disk swapping mechanism for the BF consumption queue may be used. This is still an alpha version. The download links for all the Murphi versions from the Univ of Roma are below.
Download:
Distributed Explicit State Model Checker based on Erlang and Murphi
Information & Download:
Eddy Murphi is the most current development of Murphi, and was developed in the Gauss group at the University of Utah (led by Igor Mellatti). Eddy Murphi has a separate web page here, but is included here for completeness.
Eddy Murphi is a parallel and distributed version of Murphi that utilizes MPI for communication and coordination among the compute nodes involved the verification. Further, is uses the novel Eddy algorithm to achieve a high degree of parallelism in its computation. Eddy Murphi is also derived from Caching Murphi (CMurphi).
Downloads of Eddy Murphi are kept at the main Eddy Murphi download page.
Standard Murphi is the original version of Murphi developed by Professor David Dill's group at Stanford. The latest version of Murphi has the ability to perform simulations of the described protocol as well as bredth-first and depth-first state space verification using techniques such as symmetry reduction and hash compaction. The latest downloadable version is below.
Downloads:
Related Links
These version of Murphi have been the basis of research ideas employed in the Gauss group and elsewhere. Their descriptions and download links are contained in this section.
We ported Murphi to a distributed context based on Stern & Dill's distributed model checking algorithm (they implemented it for Berkeley NOWs; we ported it to MPI). Done by Hemanthkumar Sivaraj as part of his MS thesis. Experiments based on this tool were reported in our CAV 2002, and FMCAD 2002 papers (links on main Gauss website).
The implementation of MPI we have ported to is MPICH version 1.2.2.2. The MPI port of parallel Murphi can be downloaded from here. The readme file specific to this distribution is here. Please note that this is only an alpha version and is still very much a "researchy" software.
Download:
Hemanth also developed several Random-Walk versions of Murphi for his MS. Those are recommended for furtherment by willing groups. This work was published in PDMC 2003.
We have incorporated some parallel random walks based heuristics inside Murphi for semi-formal verification. The alpha version of the tool can be downloaded below. More details regarding this tool can be had from our publications section.
Download:
Igor Melatti also has implemented a Precision on Demand (POD) algorithm due to Robert Palmer. The Alpha version of POD-Hashing Murphi by I. Melatti is distributed. Publications on this software are pending.
These two versions of Murphi (namely pod_cmurphi 1.0 and pod_3murphi 1.0) are able to improve state space coverage when using techniques leading to positive state omission probability (i.e. hash compaction and Bloom filters). This is still an alpha-version.
Download:
Predicate Abstraction Murphi (PAM) is a tool written by Xiaofang Chen as part of her PhD dissertation work. This tool takes a Murphi description, and generates a file of CVC-Lite invocations to represent the transition relation in CVC-Lite, and to conduct the classical predicate-abstraction based reachability analysis. We employ the algorithm in Satyaki Das's PhD dissertation (also see Das, Dill, and Park, CAV 1999). There is a technical report based on this tool.
PAM is able to compute the abstract state space for user-provided predicates in Murphi models, i.e. to check the reachability of each predicate property. It is an over-approximation based abstraction. The algorithms we use are based on Satyaki Das's PhD thesis. It uses CVC Lite as the decision procedure. For major details, please see our technical report.
Download:
The tool called was developed by Dr. Ritwik Bhattacharya as part of his PhD dissertation to explore symbolic partial order reduction in the context of Murphi. This tool is written in Lisp, and employs Zchaff and NuSMV.
Download:
This version fixes the C3 provision bug, which incorrectly omitted large portions of the state space search. After this fix, the state space reduction is not as large as the previous version, but is more correct.
Older versions:
This version contains a bug in the C3 provision of parital order reduction that drastically under-represents the state space.
Much of the documentation for each release is within the tarball usually in the doc folder. Also, many of the project have led to publications which can usually be found on the respective author's website.
For any further questions, please contact someone from the Gauss Group.