Template:wikipedia list Template:New unreviewed article

This article lists Model Checking Tools classified by some interesting properties. Some articles about: history and introduction to Model Checking. There are some books [1] deal with model checking techniques.

Comparison of some model checking toolsEdit

Name Model Checking Equivalence checking GUI Availability
 !Plain, Probabilistic, Stochastic, ... Modelling language Properties language Supported equivalences Counter example generation   GUI   Graphical Specification Counter example visualization Software license Programming language used Platform / OS
APMC Approximate Probabilistic Reactive modules PCTL, PLTL No Yes No No FUSC C Unix & related
ARC Plain AltaRica mu-calculus No No No No FUSC ANSI C Unix & related
BANDERA Code analysis Java CTL, LTL Yes Yes Yes Yes Free Java Windows and Unix related
BLAST Code analysis C Monitor automata Yes No No No Free OCaml Windows and Unix related
CADENCE SMV Plain Cadence SMV, SMV, Verilog CTL, LTL Yes Yes No No FUSC Template:Dunno Windows and Unix related
CADP Probabilistic LOTOS AFMC SB, WB, BB, OE, STE, WTE, SE, tau*E Yes Yes Yes Yes FUSC Template:Dunno MacOS, Linux, Solaris, Windows
CWB-NC Plain and Timed CCS, CSP, LOTOS, TCCS AFMC, CTL, GCTL SB, WB, me, ME Yes Yes No No FUSC SML of New Jersey Windows and Unix related
DBRover Timed Ada, , C++, Java, VHDL, Verilog LTL, MTL No Yes Yes Yes Commercial use only Template:Dunno Windows and Unix related
DiVinE Tool Plain DVE input language LTL No Yes No No Free C/C++ Unix related
DREAM Real-time C++, Timed automata Monitor automata Yes No No No Free C++ Windows and Unix related
Edinburgh CWB Plain CCS, TCCS, SCCS Mu calculus SB, WB, BB, me, ME, OE Yes No No No FUSC SML Windows and Unix related
Expander2 Hybrid AFMC, CTL SB, OE No Yes No No Free O'Haskell Unix related
Fc2Tools Plain FC2 Template:Dunno SB, WB, BB Yes No Yes Yes Free Template:Dunno Unix related
GEAR Plain Template:Dunno AFMC, CTL, mu-calculus Yes Yes Yes Yes Free Java Windows and Unix related
LTSA Plain FSP LTL Yes Yes No Yes Free Template:Dunno Windows and Unix related
MCMAS Plain, Epistemic ISPL CTL, CTLK Yes Yes No Yes Free C++ Unix, Windows, Mac-OS
mCRL2 Real-time mCRL2 mCRL2 mu-calculus SB, BB, t*E, STE, WTE Yes Yes No Yes Free C++ MacOS, Linux, Solaris, Windows
MRMC Real-time, Probabilistic Plain MC CSL, CSRL, PCTL, PRCTL SB No No No No Free C Windows, Linux, MacOS
PRISM Probabilistic PEPA, PRISM language, Plain MC PLTL, PCTL No Yes No No Free C++, Java Windows, Linux, MacOS
Reactis Tester Hybrid Simulink/Stateflow Template:Dunno No Yes Yes No Commercial use only Template:Dunno Windows, Linux
SPIN Plain Promela LTL No Yes No No FUSC C, C++ Windows and Unix related
TAPAs Plain CCSP CTL, mu calculus SB, WB, BB, STE, WTE, me, ME, OE Yes Yes Yes Yes Free Java Windows, MacOS and Unix related
UPPAAL Real-time Timed automata, C subset TCTL subset No Yes Yes Yes FUSC C++, Java Windows, Linux

Modelling languagesEdit

  • AltaRica: a language designed to model both functional and dysfunctional behaviours of critical systems.
  • Cadence SMV: Cadence SMV Input Language; synchronous modeling language that has features supporting SMV's style of compositional refinement verification and abstract interpretation.
  • CCS: Calculus of communicating systems; process calculus introduced by Robin Milner around 1980 and the title of a book describing the calculus.
  • CCSP: A process calculus obtained from CCS by incorporating some operators of CSP. It is defined by Olderog and by van Glabbeek/Vaandrager .
  • CSP: Communicating sequential processes; formal language for describing patterns of interaction in concurrent systems. FDR2 is a refinement checking tool for CSP, comparing two models for compatibility.
  • DVE input language: a system is described as Network of Extended Finite State Machines communicating via shared variables and unbuffered channels. Does not contain support for buffered channels and for checking the type of message to be received without performing the receive proper.
  • FC2: Machine-level ASCII representation for synchronized (hierarchical) networks of automata. Defined by the Esprit Basic Research Action CONCUR, 1992. Used as an input and exchange format by a number of verification tools, mainly in the area of process algebras.
  • FSP: Finite State Processes.
  • Java: Object-oriented programming language.
  • LOTOS: Language Of Temporal Ordering Specification (ISO standard 8807); formal specification language based on temporal ordering used for protocol specification in ISO OSI standards.
  • PEPA: Performance Evaluation Process Algebra; itis a stochastic process algebra designed for modelling computer and communication systems.
  • Plain MC: these are simple text-file formats used in MRMC and PRISM.
  • PRISM language: PRISM model description language.
  • Promela: Process or Protocol Meta Language; it is a verification modeling language. The language allows for the dynamic creation of concurrent processes to model, for example, distributed systems.
  • Reactive modules: Component-based modeling language for synchronous and asynchronous hardware and software systems.
  • Simulink/Stateflow: interactive design and simulation tool for event-driven systems.
  • SCCS: Synchronous calculus of communicating systems.
  • SMV:SMV input language.
  • TCCS: Timed CCS.
  • Verilog: an hardware description language (HDL) used to model electronic systems.
  • VHDL: commonly used as a design-entry language for field-programmable gate arrays and application-specific integrated circuits in electronic design automation of digital circuits.

Properties languageEdit

  • AFMC: Alternation Free Modal mu-Calculus.
  • CSL: Continuous Stochastic Logic, characterizes bisimulation of continuous-time Markov processes.
  • CSRL: Continuous Stochastic Reward Logic; a logic to specify measures over CTMCs extended with a reward structure (so-called Markov reward models).
  • CTL: Computation Tree Logic; a branching-time logic, meaning that its model of time is a tree-like structure in which the future is not determined; there are different paths in the future, any one of which might be an actual path that is realized.
  • GCTL: Generalized Computation Tree Logic, it's both state based and action based.
  • LTL: Linear temporal logic; a modal temporal logic with modalities referring to time.
  • Monitor automata: ???.
  • mCRL2 mu-calculus: Kozen's propositional modal mu-calculus (excluding atomic propositions), extended with: - data-depended processes - quantification over data types - multi actions - time - regular formulas.
  • mu-calculus: temporal logics with a least fix-point operator μ.
  • PCTL: Probabilistic CTL; an extension of CTL which allows for probabilistic quantification of described properties.
  • PLTL: Probabilistic Linear Temporal Logic.
  • PRCTL: Probabilistic Reward Computation Tree Logic; it extends PCTL with reward-bounded properties.



  • SB: Strong Bisimulation
  • WB: Weak Bisimulation
  • BB: Branching Bisimulation
  • STE: Strong Trace Equivalence
  • WTE: Weak Trace Equivalence
  • me: May Equivalence
  • ME: Must Equivalence
  • OE: Observational Equivalence
  • SE: Safety Equivalence
  • t*E: tau*.a Equivalence

Software license:

  • FUSC: Free Under Specific Condition

External linksEdit

  • Tools: a database for verification tools

Cite error: <ref> tags exist, but no <references/> tag was found

Ad blocker interference detected!

Wikia is a free-to-use site that makes money from advertising. We have a modified experience for viewers using ad blockers

Wikia is not accessible if you’ve made further modifications. Remove the custom ad blocker rule(s) and the page will load as expected.