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

formal_models_environments [Le 28/01/2012 à 11:44]
DavidMentre création
— (Version actuelle)
Ligne 1: Ligne 1:
-===== Tools to make formal models ===== 
-\\ 
  
-==== Alloy ==== 
-\\ 
-The Alloy Analyzer is a tool developed by the Software Design Group for analyzing models written in Alloy, a simple structural modeling language based on first-order logic. The tool can generate instances of invariants, simulate the execution of operations (even those defined implicitly), and check user-specified properties of a model. Alloy and its analyzer have been used primarily to explore abstract software designs. Its use in analyzing code for conformance to a specification and as an automatic test case generator are being investigated in ongoing research projects.\\ 
- 
-    * License: GNU GPL\\ 
-    * Web site: http://alloy.mit.edu/\\ 
- 
-==== mCRL2 ==== 
-\\ 
-mCRL2 is a formal specification language with an associated toolset. The toolset can be used for modelling, validation and verification of concurrent systems and protocols.\\ 
- 
-The toolset supports a collection of tools for linearisation, simulation, state-space exploration and generation and tools to optimise and analyse specifications. Moreover, state spaces can be manipulated, visualised and analysed.\\ 
- 
-    * License: BSD like\\ 
-    * Web site: http://www.mcrl2.org\\ 
- 
-==== TLA+ Proof System ==== 
-\\ 
-The TLA+ Proof System (TLAPS) is a platform for computerized verification of TLA+  proofs using formal reasoning systems such as automated theorem provers, proof-assistants, SMT/SAT solvers, and decision procedures. TLA+ is a specification language designed for concurrent, distributed, reactive and real-time systems, but it can also be used to formalize any discrete algorithm. The TLA+ proof language is declarative, hierarchical, and scalable to large system specifications. It provides a consistent abstraction over the various “backend” verifiers. The current release of TLAPS handles just enough temporal reasoning to check safety properties; an extension to the full TLA+ language is under active development.\\ 
- 
-    * License: BSD\\ 
-    * Web site: http://msr-inria.inria.fr/~doligez/tlaps/ 
 
formal_models_environments.1327747483.txt.gz · Dernière modification: Le 13/02/2012 à 21:07 (modification externe)     Haut de page
Recent changes RSS feed Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki Design by Chirripó