| Daftar/Tabel -- model checking toolsThis article lists model checking tools classified by some interesting properties. Some articles about: history[1] and introduction[2] to Model Checking. There are some books[3] that deal with model checking techniques. For more general tools see Daftar/Tabel -- Modeling Tools. Perbandingan -- some model checking toolsName | 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 | μ-calculus CTL* | | Yes | Yes | 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 | ? | Windows and Unix related | CADP | Probabilistic | LOTOS, FSP, LOTOS NT | AFMC | SB, WB, BB, OE, STE, WTE, SE, tau*E | Yes | Yes | Yes | Yes | FUSC | ? | MacOS, Linux, Solaris, Windows | CBMC | Code analysis | C, C++ | Assertions | | Yes | Yes | No | No | Free | C++ | Windows and Unix related | CPAchecker | Code analyses | C | Monitor automata | | Yes | Yes | No | Yes | Free | Java | Any | CWB-NC | Plain and Timed | CCS, CSP, LOTOS, TCCS | AFMC, CTL, GCTL | SB, WB, me, ME | Yes | Yes | No | No | FUSC | SML | Windows and Unix related | DBRover | Timed | Ada, C, C++, Java, VHDL, Verilog | LTL, MTL | | No | Yes | Yes | Yes | Non-freeCommercial use only | ? | Windows and Unix related | DiVinE Tool | Plain | DVE input language, C/C++ (via LLVM bitcode), Timed automata | LTL | | Yes | Yes | No | Yes | Free | C/C++ | Unix, Windows | DREAM | Real-time | C++, Timed automata | Monitor automata | | Yes | No | No | No | Free | C++ | Windows and Unix related | Edinburgh CWB | Plain | CCS, TCCS, SCCS | μ-calculus | SB, WB, BB, me, ME, OE | Yes | No | No | No | FUSC | SML | Windows and Unix related | EmbeddedValidator | Hybrid | Simulink/Stateflow/TargetLink/C | Monitor automata | | Yes | Yes | Yes | Yes | Non-freeCommercial use only | ? | Windows | Expander2 | Hybrid | | AFMC, CTL | SB, OE | No | Yes | No | No | Free | O'Haskell | Unix related | Fc2Tools | Plain | FC2 | ? | SB, WB, BB | Yes | No | Yes | Yes | Free | ? | Unix related | GEAR | Plain | ? | AFMC, CTL, μ-calculus | | Yes | Yes | Yes | Yes | Free | Java | Windows and Unix related | ImProve | Plain | Haskell | Assertions | | Yes | No | No | No | Free | Haskell | Linux, Windows, Mac-OS | Java Pathfinder | Plain and timed | Java | unknown | | No | Yes | No | No | NOSA | Java | MacOS, Windows, Linux | LLBMC | Code analysis | C (, C++, all languages supported by LLVM) | Assertions | | Yes | No | No | No | FUSC | C++ | Windows and Unix related | LTSA | Plain | FSP | LTL | | Yes | Yes | No | Yes | Free | Java | Windows and Unix related | LTSmin | Plain, Real-time | Promela, μCRL, mCRL2, DVE Input Language | μ-calculus, LTL, CTL* | SB, BB | Yes | No | No | No | Free | C, C++ | Unix, MacOSX, Windows | MCMAS | Plain, Epistemic | ISPL | CTL, CTLK | | Yes | Yes | No | Yes | Free | C++ | Unix, Windows, Mac-OS | mCRL2 | Plain, 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 | NuSMV | Plain | SMV | CTL, LTL, PSL | | Yes | No | No | No | Free | C | Unix, Windows, MacOSX | ompca, OpenMP C Analysis | software symbolic simulation with API control | C/C++ programs with OpenMP directives | logic predicates or flexible procedures through API | | Yes | Yes | No | Yes | Free | C, C++ | Ubuntu Linux, Windows version available soon | PAT | Plain,Real-time,Probabilistic | CSP#, Timed CSP, Probablilistic CSP | LTL, Assertions | | Yes | Yes | Yes | Yes | Free | C# | Windows, other OS with Mono | PRISM | Probabilistic | PEPA, PRISM language, Plain MC | CSL, PLTL, PCTL | | No | Yes | No | No | Free | C++, Java | Windows, Linux, MacOS | Reactis Tester | Hybrid | Simulink/Stateflow | ? | | No | Yes | Yes | No | Non-freeCommercial use only | SML | Windows, Linux | RED | dense-time, linear hybrid, fully symbolic | communicating timed automata (CTA), linear-hybrid automata (LHA) | TCTL with fairness assumptions, CTA with fairness assumptions | timed simuilation, fair simulation | Yes | Yes | Yes | Yes | Free | C/C++ | Ubuntu Linux | SATABS | Code analysis | C, C++ | Assertions | | Yes | Yes | No | No | Free | C++ | Windows and Unix related | SLMC | Plain | pi-calculus | CCL | | Yes | No | No | No | Free | OCAML | Windows and Unix related | SPIN | Plain | Promela | LTL | | Yes | Yes | No | Yes | FUSC | C, C++ | Windows and Unix related | Spot | Plain | Petri nets, DVE Input Language | LTL, PSL subset | | Yes | No | No | No | Free | C, C++ | Unix & related | TAPAAL | Real-time | Timed-Arc Petri Nets, age invariants, inhibitor arcs, transport arcs | TCTL subset | | No | Yes | Yes | Yes | Free | C++, Java | MacOS, Windows, Linux | TAPAs | Plain | CCSP | CTL, μ-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 | | Yes | Yes | Yes | Yes | FUSC | C++, Java | MacOS, Windows, Linux | ROMEO | Real-time | Time Petri Nets, stopwatch parametric Petri nets | TCTL subset | | Yes | Yes | Yes | No | Free | C++, tcl/tk | MacOS, Windows, Linux | TLC | Plain | TLA+, PlusCal | TLA | | Yes | Yes | Yes | No | Free | Java | 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; 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[4] and by van Glabbeek/Vaandrager.[5]
- 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; 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: 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: an interactive design and simulation tool for event-driven systems.
- SCCS: synchronous calculus of communicating systems.
- SMV: SMV input language.
- TCCS: Timed CCS.
- Verilog: 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: 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; 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.
- PSL: Property specification language
AbbreviationsEquivalences: - 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
References External links- Tools: a database for verification tools
|
| |