This article's use of external links may not follow Wikipedia's policies or guidelines. (December 2021) |
Murφ (/ˈmɝ.fi/, also spelled Murphi) is an explicit-state model checker developed at Stanford University, and widely used for formal verification of cache-coherence protocols.
| Developer(s) | David Dill's research group at the Stanford University Computer Systems Laboratory |
|---|---|
| Stable release | 3.1
/ November 1993 |
| Repository | github |
| Written in | ANSI C++ |
| Operating system | Linux |
| Type | Model Checking |
| License | similar to the MIT license |
| Website | http://verify.stanford.edu/dill/murphi.html (via the Wayback Machine) |
History
editMurφ's early history is described in a paper by David Dill.[1] The first version of Murφ was designed at Stanford University in 1990 and 1991 by Prof. David Dill and his graduate students Andreas Drexler, Alan Hu, and Han Yang, and primarily implemented by Andreas Drexler. The specification language was extensively modified and extended by David Dill, Alan Hu, C. Norris Ip, Ralph Melton, Seungjoon Park, and Han Yang. Ralph Melton implemented the new version during the summer and fall of 1992. Seungjoon Park added liveness checking and fairness constraints, but because the algorithm for liveness verification conflicted with important optimizations, particularly symmetry reduction, liveness verification was omitted in subsequent releases. C. Norris Ip implemented reversible rules and repetition constructors (which are not included in release 3.1), and added symmetry and multiset reductions (which are). Ulrich Stern implemented hash compaction,[2] improved the use of disk, and implemented Parallel Murφ.
The last release from Stanford was release 3.1 in November of 1993. Many derivative versions of Murφ have been created since then by other groups.
Features
editThe Murφ compiler accepts a model written in the Murφ specification language and outputs C++ code that constitutes a verifier for that model. (That is, the C++ code, when executed, performs explicit-state model checking on the design described by the specification.) The Murφ specification language uses guarded commands and an asynchronous, interleaving model of concurrency, with all synchronization and communication done through global variables. The verifier checks safety properties in the form of invariants and internal assertions that are specified in the model, and checks for deadlock. It does not check liveness properties, though Murφ release 2.7L did support verification of a set of common LTL liveness properties. The language and verifier support some kinds of symmetry reductions.[3]
Murφ was originally applied to verifying cache-coherence protocols,[4] but has been applied to other problems as well, including verification of security protocols.
Licensing
editThe Murφ license is similar to the MIT license. Murφ may be used, copied, modified, sold, and redistributed for any purpose, provided the copyright notice and license are included, the name of Stanford University is not used for advertising or publicity without permission, and modified versions are not called Murphi without permission.
Derivatives
editMany derivative versions of Murφ have been created, at Stanford and elsewhere, including these:
- Parallel Murφ
- Eddy — Parallel and distributed Murφ.
- PReach (Parallel Reachability) — Parallel model checking implemented in Erlang.
- Distributed Murphi
- Parallel Random-Walk Murphi
- PAM — Predicate Abstraction Murphi
- POeM — Partial-Order Enabled Murphi
- CMurphi — Caching Murphi.
- FHP-Murphi — Finite Horizon Probabilistic Murphi.
- Eddy Murphi — Parallel and distributed, based on CMurphi, using MPI for message passing.
- Universal Planner Murphi — Planning and universal planning for linear and nonlinear continuous PDDL+ models with processes and events; also timed initial literals and timed initial fluents.
- rumur
See also
editReferences
edit- ^ Dill, David L. (2008). Grumberg, Orna; Veith, Helmut (eds.). 25 Years of Model Checking: History, Achievements, Perspectives. pp. 77–88.
- ^ Stern, Ulrich; Dill, David L. (1996). Formal Description Techniques IX. Boston, MA: Springer. pp. 333–348.
- ^ Ip, C. Norris; Dill, David L. (1993). "Efficient verification of symmetric concurrent systems". Proceedings of 1993 IEEE International Conference on Computer Design ICCD'93. IEEE. pp. 230–234. doi:10.1109/ICCD.1993.393375. ISBN 0-8186-4230-0. S2CID 38444364.
- ^ Dill, David L.; Drexler, Andreas J.; Hu, Alan J.; Yang, C. Han (1992). "Protocol verification as a hardware design aid". Proceedings of the 1992 IEEE International Conference on Computer Design: VLSI in Computers & Processors. IEEE: 552–525.