List of model checking tools

Last updated

This article lists model checking tools and gives an overview of the functionality of each.

Contents

Overview of some model checking tools

The following table includes model checkers that have

  1. a web site from which it can be downloaded,
  2. a declared license,
  3. a description published in archived literature, and
  4. a Wikipedia article describing it.

In the below table, the following abbreviations are used:

NameModel CheckingEquivalence checkingGUIAvailability
Plain, Probabilistic, Stochastic, ...Modelling languageProperties languageSupported equivalencesCounter example generation  GUI  Graphical SpecificationCounter example visualizationSoftware licenseProgramming language usedPlatform, OS
BLAST Code analysis C Monitor automataYesNoNoNoFree OCaml Windows, Unix related
CADP Plain and probabilistic LOTOS, FC2, FSP, LNTAFMC, MCL, XTLSB, WB, BB, OE, STE, WTE, SE, tau*EYesYesNoYesFUSC C, Bourne shell, Tcl/Tk, LOTOS, LNTmacOS, Linux, Solaris, Windows
CPAchecker Code analysis C Monitor automataYesYesNoYesFreeJavaAny
DREAM Real-time C++, Timed automata Monitor automataYesNoNoNoFree C++ Windows, Unix related
FizzBee Specification LanguagePlain and probabilistic Python LTL YesYesNoYesFree Go macOS, Windows, Linux
GreatSPN Plain, probabilistic, real-time, stochasticTime Petri Nets, Stochastic Petri Nets, Colored Petri Nets, Well-formed Petri Nets LTL, CTL, CTL*, CSL, CSLTANoYesYesNoFree C, C++, Java macOS, Windows, Linux
Java Pathfinder Plain and timedJavaunknownNoYesNoNoOpen Source Agreement Java macOS, Windows, Linux
Murφ (Murphi) PlainMurφInvariants, assertionsYesNoNoNoFree C++ Linux
NuSMV PlainSMV input language CTL, LTL, PSL YesNoNoNoFree C Unix, Windows, macOS
PAT Plain, real-time, probabilistic CSP#, timed CSP, probabilistic CSP LTL, assertions YesYesYesYesFree C# Windows, others with Mono
PRISM Probabilistic PEPA, PRISM language, Plain MCCSL, PLTL, PCTL NoYesNoNoFree C++, Java Windows, Linux, macOS
Rumur PlainMurφInvariants, assertionsYesNoNoNoFree C macOS, Linux
SPIN Plain Promela LTL YesYesNoYesFUSC C, C++ Windows, Unix related
TAPAAL Real-timeTimed-Arc Petri Nets, age invariants, inhibitor arcs, transport arcsTCTL subsetNoYesYesYesFree C++, Java macOS, Windows, Linux
TAPAs PlainCCSP CTL, μ-calculus SB, WB, BB, STE, WTE, me, ME, OEYesYesYesYesFree Java Windows, macOS, Unix related
UPPAAL Real-time Timed automata, C subsetTCTL subsetYesYesYesYesFUSC C++, Java macOS, Windows, Linux
ROMEO Real-timeTime Petri Nets, stopwatch parametric Petri netsTCTL subsetYesYesYesNoFree C++, Tcl/Tk macOS, Windows, Linux
TLA+ Model Checker (TLC)Plain TLA+, PlusCal TLA YesYesYesNoFree Java macOS, Windows, Linux

Modelling languages

Properties language

Comparison of model checking tools

Scientific publications

There exists a few papers that systematically compare various model checkers on a common case study. The comparison usually discusses the modelling tradeoffs faced when using the input languages of each model checker, as well as the comparison of performances of the tools when verifying correctness properties. One can mention:

International software competitions

See also

References

  1. E.R. Olderog: Operational Petri net semantics for CCSP
  2. Rob van Glabbeek, Frits Vaandrager: Bundle Event Structures and CCSP
  3. Romijn, Judi (June 1999). Model Checking a HAVi Leader Election Protocol (Technical report). Amsterdam: CWI. SEN-R9915. Archived from the original on 2019-09-11. Retrieved 2018-06-14.
  4. Dong, Yifei; Du, Xiaoqun; Holzmann, Gerard; Smolka, Scott (2003). "Fighting Livelock in the GNU i-Protocol: A Case Study in Explicit-State Model Checking". Software Tool for Technology Transfer. 4 (4): 505–528.
  5. Bortnik, Elena M.; Trcka, Nikola; Wijs, Anton; Luttik, Bas; van de Mortel-Fronczak, J. M.; Baeten, Jos C. M.; Fokkink, Wan; Rooda, J. E. (2005). "Analyzing a chi model of a turntable system using Spin, CADP and Uppaal" (PDF). Journal of Logical and Algebraic Methods in Programming. 65 (2): 51–104. doi: 10.1016/j.jlap.2005.05.001 . Archived (PDF) from the original on 2021-01-27. Retrieved 2018-05-25.
  6. Mazzanti, Franco; Ferrari, Alessio (2018). "Ten Diverse Formal Models for a CBTC Automatic Train Supervision System". Proceedings of the 3rd Workshop on Models for Formal Analysis of Real Systems and 6th International Workshop on Verification and Program Transformation (MARS/VPT’18), Thessaloniki, Greece. Electronic Proceedings in Theoretical Computer Science. Vol. 268. pp. 104–149. arXiv: 1803.10324v1 . doi:10.4204/EPTCS.268.4.
Common benchmarks