Différences

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

Lien vers cette vue

model_checkers [Le 20/12/2012 à 16:30]
david_mentre
— (Version actuelle)
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. 
  
 
model_checkers.1356017409.txt.gz · Dernière modification: Le 20/12/2012 à 16:30 par david_mentre     Haut de page
Recent changes RSS feed Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki Design by Chirripó