List of model checking tools - AbsoluteAstronomy.com

This article lists model checking
Model checking
In computer science, model checking refers to the following problem:Given a model of a system, test automatically whether this model meets a given specification....

tools classified by some interesting properties.
Some articles about: history and introduction to Model Checking.
There are some books that deal with model checking techniques.

Comparison of some model checking tools

{| class="wikitable" style="text-align:center;"
|-
!Name !! colspan="3" | Model Checking !! colspan="2" | Equivalence checking !!colspan="3"| GUI !! colspan="3"| Availability
|- style="font-size:70%"
!
!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
This article lists model checking
Model checking
In computer science, model checking refers to the following problem:Given a model of a system, test automatically whether this model meets a given specification....

tools classified by some interesting properties.
Some articles about: history and introduction to Model Checking.
There are some books that deal with model checking techniques.

Comparison of some model checking tools

{| class="wikitable" style="text-align:center;"
|-
!Name !! colspan="3" | Model Checking !! colspan="2" | Equivalence checking !!colspan="3"| GUI !! colspan="3"| Availability
|- style="font-size:70%"
!
!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

This article lists model checking
Model checking
In computer science, model checking refers to the following problem:Given a model of a system, test automatically whether this model meets a given specification....

tools classified by some interesting properties.
Some articles about: history and introduction to Model Checking.
There are some books that deal with model checking techniques.

Comparison of some model checking tools

Probabilistic CTL

Probabilistic Computation Tree Logic is an extension of CTL which allows for probabilistic quantification of described properties. It has been defined in the paper by ....

C (programming language)

C is a general-purpose computer programming language developed between 1969 and 1973 by Dennis Ritchie at the Bell Telephone Laboratories for use with the Unix operating system....

C (programming language)

C is a general-purpose computer programming language developed between 1969 and 1973 by Dennis Ritchie at the Bell Telephone Laboratories for use with the Unix operating system....

Java (programming language)

Java is a programming language originally developed by James Gosling at Sun Microsystems and released in 1995 as a core component of Sun Microsystems' Java platform. The language derives much of its syntax from C and C++ but has a simpler object model and fewer low-level facilities...

| CTL, LTL

Linear temporal logic

In logic, Linear temporal logic is a modal temporal logic with modalities referring to time. In LTL, one can encode formulae about the future of paths such as that a condition will eventually be true, that a condition will be true until another fact becomes true, etc. It is a fragment of the more...

Java (programming language)

|Windows and Unix related

|-
| BLAST

BLAST model checker

The Berkeley Lazy Abstraction Software Verification Tool is a software model checking tool for C programs. The task addressed by BLAST is the need to check whether software satisfies the behavioral requirements of its associated interfaces...

| Code analysis
| C

C (programming language)

C is a general-purpose computer programming language developed between 1969 and 1973 by Dennis Ritchie at the Bell Telephone Laboratories for use with the Unix operating system....

Objective Caml

OCaml , originally known as Objective Caml, is the main implementation of the Caml programming language, created by Xavier Leroy, Jérôme Vouillon, Damien Doligez, Didier Rémy and others in 1996...

Verilog

In the semiconductor and electronic design industry, Verilog is a hardware description language used to model electronic systems. Verilog HDL, not to be confused with VHDL , is most commonly used in the design, verification, and implementation of digital logic chips at the register-transfer level...

|CTL, LTL

Linear temporal logic

Language Of Temporal Ordering Specification

Language Of Temporal Ordering Specification is a formal specification language based on temporal ordering used for protocol specification in ISO OSI standards....

C (programming language)

C is a general-purpose computer programming language developed between 1969 and 1973 by Dennis Ritchie at the Bell Telephone Laboratories for use with the Unix operating system....

, C++

C++

C++ is a statically typed, free-form, multi-paradigm, compiled, general-purpose programming language. It is regarded as an intermediate-level language, as it comprises a combination of both high-level and low-level language features. It was developed by Bjarne Stroustrup starting in 1979 at Bell...

| Assertions

Assertion (computing)

In computer programming, an assertion is a predicate placed in a program to indicate that the developer thinks that the predicate is always true at that place.For example, the following code contains two assertions:...

| style="font-size:70%; text-align:left;"|
|
|
|
|
|
|C++

C++

C (programming language)

C is a general-purpose computer programming language developed between 1969 and 1973 by Dennis Ritchie at the Bell Telephone Laboratories for use with the Unix operating system....

| Monitor automata
| style="font-size:70%" align=left |
|
|
|
|?
|
|Java
|Any

|-
| CWB-NC
| Plain and Timed
| CCS

Calculus of Communicating Systems

The Calculus of Communicating Systems is a process calculus introduced by Robin Milner around 1980 and the title of a book describing the calculus. Its actions model indivisible communications between exactly two participants. The formal language includes primitives for describing parallel...

, CSP

Communicating sequential processes

In computer science, Communicating Sequential Processes is a formal language for describing patterns of interaction in concurrent systems. It is a member of the family of mathematical theories of concurrency known as process algebras, or process calculi...

, LOTOS

Language Of Temporal Ordering Specification

Language Of Temporal Ordering Specification is a formal specification language based on temporal ordering used for protocol specification in ISO OSI standards....

Ada (programming language)

Ada is a structured, statically typed, imperative, wide-spectrum, and object-oriented high-level computer programming language, extended from Pascal and other languages...

, C

C (programming language)

C is a general-purpose computer programming language developed between 1969 and 1973 by Dennis Ritchie at the Bell Telephone Laboratories for use with the Unix operating system....

, C++

C++

, Java

Java (programming language)

, VHDL, Verilog

Verilog

| LTL

Linear temporal logic

Linear temporal logic

|
|
|
|
|
|
|C

C (programming language)

C is a general-purpose computer programming language developed between 1969 and 1973 by Dennis Ritchie at the Bell Telephone Laboratories for use with the Unix operating system....

/C++

C++

|Unix, Windows

|-
| DREAM

DREAM (software)

The Distributed Real-time Embedded Analysis Method is a platform-independent open-source tool for the verification and analysis of distributed real-time and embedded systems which focuses on the practical application of formal verification and timing analysis to real-time middleware...

| Real-time
| C++

C++

C++

Calculus of Communicating Systems

Standard ML

Standard ML is a general-purpose, modular, functional programming language with compile-time type checking and type inference. It is popular among compiler writers and programming language researchers, as well as in the development of theorem provers.SML is a modern descendant of the ML...

Java (programming language)

Haskell (programming language)

Haskell is a standardized, general-purpose purely functional programming language, with non-strict semantics and strong static typing. It is named after logician Haskell Curry. In Haskell, "a function is a first-class citizen" of the programming language. As a functional programming language, the...

| Assertions

Assertion (computing)

Haskell (programming language)

|Linux, Windows, Mac-OS

|-
| LTSA
| Plain
| FSP
| LTL

Linear temporal logic

Promela

PROMELA is a verification modeling language. The language allows for the dynamic creation of concurrent processes to model, for example, distributed systems. In PROMELA models, communication via message channels can be defined to be synchronous , or asynchronous...

, mCRL2

MCRL2

mCRL2 is a specification language for describing concurrent discrete event systems. It is accompanied with a toolset, that facilitates tools, techniques and methods for simulation, analysis and visualization of behaviour. The behavioural part of the language is based on process algebra...

, NIPS-VM, DVE Input Language
| μ-calculus, LTL

Linear temporal logic

, CTL*
| SB, BB
|
|
|
|
|
|C

C (programming language)

C is a general-purpose computer programming language developed between 1969 and 1973 by Dennis Ritchie at the Bell Telephone Laboratories for use with the Unix operating system....

C++

| Unix, Windows, Mac-OS

|-
| mCRL2

MCRL2

| Real-time
| mCRL2

MCRL2

C++

|MacOS, Linux, Solaris, Windows

|-
| MRMC

Markov Reward Model Checker (MRMC)

The Markov Reward Model Checker is a model checker for discrete-time and continuous-time Markov reward models. It supports reward extensions of PCTL and , and allows for the automated verification of properties concerning long-run and instantaneous rewards as well as cumulative rewards...

C (programming language)

C is a general-purpose computer programming language developed between 1969 and 1973 by Dennis Ritchie at the Bell Telephone Laboratories for use with the Unix operating system....

|Windows, Linux, MacOS

|-
| NuSMV

NuSMV

- Introduction :NuSMV is a reimplementation and extension of SMV symbolic model checker, the first model checking tool based on Binary Decision Diagrams .The tool has been designed as an open architecture for model checking...

| Plain
| SMV
| CTL, LTL

Linear temporal logic

, PSL

Property Specification Language

Property Specification Language is a language developed by Accellera for specifying properties or assertions about hardware designs. The properties can then be simulated or formally verified. Since September 2004 the standardization on the language has been done in IEEE 1850 working group...

|
|
|
|
|
|
| C

C (programming language)

C is a general-purpose computer programming language developed between 1969 and 1973 by Dennis Ritchie at the Bell Telephone Laboratories for use with the Unix operating system....

C (programming language)

C is a general-purpose computer programming language developed between 1969 and 1973 by Dennis Ritchie at the Bell Telephone Laboratories for use with the Unix operating system....

, C++

C++

| Ubuntu Linux, Windows version available soon

|-
| PAT

PAT (model checker)

PAT is a self-contained framework for composing, simulating and reasoning of concurrent, real-time systems and other possible domains. It comes with user friendly interfaces, featured model editor and animated simulator...

| Plain,Real-time,Probabilistic
| CSP#, Timed CSP, Probablilistic CSP
| LTL

Linear temporal logic

, Assertions

Assertion (computing)

|
|
|
|
|
|
| C#
| Windows, other OS with Mono

|-
| PRISM

PRISM (model checker)

PRISM is a probabilistic model checker, a formal verification software tool for the modelling and analysis of systems that exhibit probabilistic behaviour . One source of such systems is the use of randomization, for example in communication protocols like Bluetooth and FireWire, or in security...

| Probabilistic
| PEPA

PEPA

Performance Evaluation Process Algebra is a stochastic process algebra designed for modelling computer and communication systems introduced by Jane Hillston in the 1990s...

C++

, Java

Java (programming language)

Stateflow

Stateflow, developed by MathWorks, is a control logic tool used to model reactive systems via state charts and flow diagrams within a Simulink model...

C (programming language)

C is a general-purpose computer programming language developed between 1969 and 1973 by Dennis Ritchie at the Bell Telephone Laboratories for use with the Unix operating system....

, C++

C++

| Assertions

Assertion (computing)

| style="font-size:70%; text-align:left;"|
|
|
|
|
|
|C++

C++

Pi-calculus

In theoretical computer science, the π-calculus is a process calculus originally developed by Robin Milner, and David Walker as a continuation of work on the process calculus CCS...

SPIN model checker

SPIN is a general tool for verifying the correctness of distributed software models in a rigorous and mostly automated fashion. It was written by Gerard J. Holzmann and others in the original Unix group of the Computing Sciences Research Center at Bell Labs, beginning in 1980...

| Plain
| Promela

Promela

| LTL

Linear temporal logic

|
|
|
|
|
|
|C

C (programming language)

C is a general-purpose computer programming language developed between 1969 and 1973 by Dennis Ritchie at the Bell Telephone Laboratories for use with the Unix operating system....

, C++

C++

|Windows and Unix related

|-
| TAPAs

TAPAs model checker

' is a tool for specifying and analyzing concurrent systems, its aim is to support teaching of process algebras. Systems are described as process algebras terms that are then mapped to Labeled Transition Systems...

Java (programming language)

|Windows, MacOS and Unix related

|-
| UPPAAL

Uppaal Model Checker

Uppaal is an integrated tool environment for modeling, validation and verification of real-time systems modeled as networks of timed automata, extended with data types ....

C++

, Java

Java (programming language)

|MacOS, Windows, Linux

|-
| ROMEO

Romeo Model Checker

Roméo is an integrated tool environment for modeling, validation and verification of real-time systems modeled as time Petri Nets or stopwtach Petri Nets, extended with parameters ....

C++

PlusCal

PlusCal is an algorithmic language. It is designed to replace pseudocode. PlusCal can express both sequential and concurrent algorithms and features means to handle nondeterminism, atomicity and model checking.- Syntax :...

| TLA

Temporal Logic of Actions

Temporal logic of actions is a logic developed by Leslie Lamport, which combines temporal logic with a logic of actions.It is used to describe behaviours of concurrent systems.- Details :...

Java (programming language)

|Windows, Linux

|}

Modelling languages

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
The Calculus of Communicating Systems is a process calculus introduced by Robin Milner around 1980 and the title of a book describing the calculus. Its actions model indivisible communications between exactly two participants. The formal language includes primitives for describing parallel...

: 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
Calculus of Communicating Systems
The Calculus of Communicating Systems is a process calculus introduced by Robin Milner around 1980 and the title of a book describing the calculus. Its actions model indivisible communications between exactly two participants. The formal language includes primitives for describing parallel...

by incorporating some operators of CSP
Communicating sequential processes
In computer science, Communicating Sequential Processes is a formal language for describing patterns of interaction in concurrent systems. It is a member of the family of mathematical theories of concurrency known as process algebras, or process calculi...

. It is defined by Olderog and by van Glabbeek/Vaandrager.
CSP
Communicating sequential processes
In computer science, Communicating Sequential Processes is a formal language for describing patterns of interaction in concurrent systems. It is a member of the family of mathematical theories of concurrency known as process algebras, or process calculi...

: Communicating sequential processes; formal language for describing patterns of interaction in concurrent systems. FDR2
FDR2
FDR and subsequently FDR2 are refinement checking software tools, designed to check formal models expressed in Communicating sequential processes . The tools have been developed by Formal Systems Ltd...

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
Java (programming language)
Java is a programming language originally developed by James Gosling at Sun Microsystems and released in 1995 as a core component of Sun Microsystems' Java platform. The language derives much of its syntax from C and C++ but has a simpler object model and fewer low-level facilities...

: Object-oriented programming language.
LOTOS
Language Of Temporal Ordering Specification
Language Of Temporal Ordering Specification is a formal specification language based on temporal ordering used for protocol specification in ISO OSI standards....

: Language Of Temporal Ordering Specification (ISO standard 8807); formal specification language based on temporal ordering used for protocol specification in ISO OSI standards.
PEPA
PEPA
Performance Evaluation Process Algebra is a stochastic process algebra designed for modelling computer and communication systems introduced by Jane Hillston in the 1990s...

: Performance Evaluation Process Algebra; it is 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
Promela
PROMELA is a verification modeling language. The language allows for the dynamic creation of concurrent processes to model, for example, distributed systems. In PROMELA models, communication via message channels can be defined to be synchronous , or asynchronous...

: 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: a component-based modeling language for synchronous and asynchronous hardware and software systems
REDLIB: Timed CTL.
Simulink/Stateflow
Stateflow
Stateflow, developed by MathWorks, is a control logic tool used to model reactive systems via state charts and flow diagrams within a Simulink model...

: an interactive design and simulation tool for event-driven systems.
SCCS: synchronous calculus of communicating systems.
SMV: SMV input language.
TCCS: Timed CCS.
Verilog
Verilog
In the semiconductor and electronic design industry, Verilog is a hardware description language used to model electronic systems. Verilog HDL, not to be confused with VHDL , is most commonly used in the design, verification, and implementation of digital logic chips at the register-transfer level...

: a 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 language

AFMC: Alternation Free Modal mu-Calculus.
Assertions
Assertion (computing)
In computer programming, an assertion is a predicate placed in a program to indicate that the developer thinks that the predicate is always true at that place.For example, the following code contains two assertions:...

: Imperative assertion statements.
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
In logic, Linear temporal logic is a modal temporal logic with modalities referring to time. In LTL, one can encode formulae about the future of paths such as that a condition will eventually be true, that a condition will be true until another fact becomes true, etc. It is a fragment of the more...

: 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
Probabilistic Computation Tree Logic is an extension of CTL which allows for probabilistic quantification of described properties. It has been defined in the paper by ....

: 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.

Abbreviations

Equivalences:

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 links

Tools: a database for verification tools

The source of this article is wikipedia, the free encyclopedia. The text of this article is licensed under the GFDL.