# Différences

Cette page vous donne les différences entre la révision choisie et la version actuelle de la page.

— |
astuces:model_checkers [Le 30/01/2019 à 17:55] (Version actuelle) jaxom créée |
||
---|---|---|---|

Ligne 1: | Ligne 1: | ||

+ | ===== Model checkers ===== | ||

+ | \\ | ||

+ | Model checkers are tool that verify all possible states of a formal model, i.e. a formal description of a system. Compared to proof assistant, they can be less powerful but easier to use.\\ | ||

+ | |||

+ | \\ | ||

+ | ==== NuSMV ==== | ||

+ | \\ | ||

+ | %%NuSMV%%is a reimplementation and extension of SMV, the first model checker based on BDDs. %%NuSMV%%has been designed to be an open architecture for model checking, which can be reliably used for the verification of industrial designs, as a core for custom verification tools, as a testbed for formal verification techniques, and applied to other research areas.\\ | ||

+ | |||

+ | * License: GNU LGPL 2.1\\ | ||

+ | * Web site: http://nusmv.irst.itc.it/\\ | ||

+ | |||

+ | \\ | ||

+ | ==== Murphi ==== | ||

+ | \\ | ||

+ | Murphi also has a formal verifier based on explicit state enumeration. The verifier performs depth- or breadth-first search in the state graph defined by a Murphi description, storing all the states it encounters in a large hash table. When a state is generated that is already in the hash table, the search algorithm does not expand its successor states (they were expanded whenever the state was originally inserted in the table).\\ | ||

+ | |||

+ | * License: BSD like\\ | ||

+ | * Web site: http://verify.stanford.edu/dill/murphi.html\\ | ||

+ | |||

+ | \\ | ||

+ | ==== Mec 5 ==== | ||

+ | \\ | ||

+ | Mec 5 is a model-checker for finite %%AltaRica%%models, using a very expressive specification language (systems of fixpoint equations over finite relations with first-order quantifiers and equality testing).\\ | ||

+ | |||

+ | * License: Public domain\\ | ||

+ | * Web site: http://altarica.labri.fr/Tools/Mec5/\\ | ||

+ | |||

+ | ==== Maria ==== | ||

+ | \\ | ||

+ | Maria is a reachability analyzer for concurrent systems that uses Algebraic System Nets (a high-level variant of Petri nets) as its modelling formalism.\\ | ||

+ | |||

+ | * License: GNU LGPL\\ | ||

+ | * Web site: http://www.tcs.hut.fi/Software/maria/ | ||

+ | |||

+ | ==== ProB ==== | ||

+ | |||

+ | ProB is an animator and model checker for the B-Method. It allows fully automatic animation of many B specifications, and can be used to systematically check a specification for range of errors. The constraint-solving capabilities of ProB can also be used for model finding, deadlock checking and test-case generation. | ||

+ | |||

+ | In addition to B, ProB now also supports Event-B, CSP-M, TLA+, and Z. ProB can be installed within Rodin, where it comes with BMotionStudio to easily generate domain specific graphical visualizations. | ||

+ | |||

+ | ProB is now being used within Siemens and Alstom for data validation of complicated properties. Commercial support is provided by the spin-off company Formal Mind. | ||

+ | |||

+ | |||

+ | * License: Eclipse Public License | ||

+ | * Web site: http://www.stups.uni-duesseldorf.de/ProB/index.php5/The_ProB_Animator_and_Model_Checker | ||

+ | |||

+ | ==== SAL ==== | ||

+ | |||

+ | See also the [[formal_models_environments#sal|SAL environment]] that contains a model checker. | ||

+ | |||

+ | ==== Spin ==== | ||

+ | |||

+ | Spin is a popular open-source software verification tool, used by thousands of people worldwide. The tool can be used for the formal verification of multi-threaded software applications. The tool was developed at Bell Labs in the Unix group of the Computing Sciences Research Center, starting in 1980. The software has been available freely since 1991, and continues to evolve to keep pace with new developments. In April 2002 the tool was awarded the ACM System Software Award. | ||

+ | |||

+ | Some of the features that set Spin apart from related verification systems are: | ||

+ | |||

+ | * Spin targets the efficient verification of multi-threaded software, not the verification of hardware circuits. The tool supports a high level language to specify systems descriptions called PROMELA (short for: PROcess MEta LAnguage). Spin has been used to trace logical design errors in distributed systems design, such as operating systems, data communications protocols, switching systems, concurrent algorithms, railway signaling protocols, control software for spacecraft, nuclear power plants, etc. The tool checks the logical consistency of a specification and reports on deadlocks, race conditions, different types of incompleteness, and unwarranted assumptions about the relative speeds of processes. | ||

+ | |||

+ | * Spin provides direct support for the use of embedded C code as part of model specifications. This makes it possible to directly verify implementation level software specifications, using Spin as a driver and as a logic engine to verify high level temporal properties. With the help of the model extractor modex it is also possible to mechanically derive a PROMELA model from concurrent C code, and verify it with Spin. | ||

+ | |||

+ | * Spin provides direct support for the use of multi-core computers for model checking runs - supporting the verification of both safety and liveness properties. | ||

+ | |||

+ | * Spin works on-the-fly, which means that it avoids the need to preconstruct a global state graph, or Kripke structure, as a prerequisite for the verification of system properties. This makes it possible to verify very large system models. | ||

+ | |||

+ | * Spin can be used as a full LTL model checking system, supporting all correctness requirements expressible in linear time temporal logic, but it can also be used as an efficient on-the-fly verifier for more basic safety and liveness properties. Many of the latter properties can be expressed, and verified, without the use of LTL. Correctness properties can be specified as system or process invariants (using assertions), as linear temporal logic requirements (LTL), as formal Büchi automata, or more broadly as general omega-regular properties in the syntax of Spin never claims. | ||

+ | |||

+ | * The tool is one of very few verification tools that supports dynamically growing and shrinking numbers of processes, using a rubber state vector technique. | ||

+ | |||

+ | * The tool supports both rendezvous and buffered message passing, and communication through shared memory. Mixed systems, using both synchronous and asynchronous communications, are also supported. Message channel identifiers for both rendezvous and buffered channels, can be passed from one process to another in messages, which makes it possible (for instance) to verify models from mobile pi-calculus. | ||

+ | |||

+ | * The tool supports random, interactive and guided simulation, and both exhaustive and partial proof techniques, based on depth-first search, breadth-first search, or bounded context-switching. The tool is designed to scale well, and to handle large problem sizes efficiently. | ||

+ | |||

+ | * To optimize verification runs, Spin exploits efficient partial order reduction techniques, and (optionally) BDD-like state storage techniques. | ||

+ | |||

+ | * License: [[http://www.spinroot.com/spin/spin_license.html|Spin license]] | ||

+ | * **Disclaimer**: Spin is said non-free software by [[http://lists.debian.org/debian-legal/2004/01/msg00273.html|Debian]] and [[https://www.redhat.com/archives/fedora-legal-list/2009-December/msg00040.html|Fedora]] projects. Nonetheless, Spin license allows to freely redistribute source code and binaries and allow to modify the source code and redistribute it in modified form (for any purpose, including selling). Therefore [[david_mentre|I (david)]] consider it open-source tool. | ||

+ | * Web Site: http://spinroot.com | ||

+ | |||

+ | ==== Cubicle ==== | ||

+ | |||

+ | Cubicle is an open source model checker for verifying safety properties of array-based systems. This is a syntactically restricted class of parametrized transition systems with states represented as arrays indexed by an arbitrary number of processes. Cache coherence protocols and mutual exclusion algorithms are typical examples of such systems. | ||

+ | |||

+ | Cubicle model-checks by a symbolic backward reachability analysis on infinite sets of states represented by specific simple formulas, called cubes. Cubicle is based on ideas introduced by MCMT from which, in addition to revealing the implementation details, it differs in a more friendly input language and a concurrent architecture. Cubicle is written in OCaml. Its SMT solver is a tightly integrated, lightweight and enhanced version of Alt-Ergo; and its parallel implementation relies on the Functory library. | ||

+ | |||

+ | * License: Apache 2.0 | ||

+ | * Web site: http://cubicle.lri.fr/ | ||

+ | |||