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:45]
DavidMentre modification
— (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/\\ 
- 
-==== [[proof_power|ProofPower]] ==== 
-\\ 
-%%ProofPower%%is a suite of tools supporting specification and proof in Higher Order Logic (HOL) and in the Z notation. The suite comprises the following packages:\\ 
- 
-        * %%PPDev%%  * The %%ProofPower%%developer kit, mainly comprising SLRP, a parser generator for Standard ML.\\ 
-        * %%PPTex%%  * The %%ProofPower%%interface to %%TeX%%and %%LaTeX%%.\\ 
-        * PPXpp - The X Windows/Motif front-end for %%ProofPower%%.\\ 
-        * PPHol - The HOL specification and proof development system.\\ 
-        * PPZed - The Z specification and proof development system.\\ 
-        * PPDaz - The Compliance Tool for specifying and verifying Ada programs.\\ 
- 
-All the %%ProofPower%%packages except PPDaz are free, open-source, software made available under the terms of the GNU General Public License.\\ 
- 
-%%ProofPower%%has been under ongoing development since 1989. It was originally designed and implemented by International Computers Ltd. to support proofs of specification-to-model correspondence for high-assurance secure systems. It has since played an important role in approaches to specifying and verifying safety-critical systems in work by the Defence and Evaluation Research Agency, now %%QinetiQ%%, and others. Since 1997, on-going developments to the product have been undertaken by Lemma 1 Ltd. In Spring 2000, International Computers Ltd. transferred its rights in %%ProofPower%%to Lemma 1 Ltd who now maintain this web site and support and distribute the software.\\ 
- 
-  * License: GPL (except PPDaz)\\ 
-  * Web site: http://www.lemma-one.com/ProofPower/index/index.html\\ 
- 
-\\ 
-==== K ==== 
-\\ 
-K is a rewrite-based executable semantic framework in which programming languages, type systems and formal analysis tools can be defined using configurations, computations and rules. Configurations organize the state in units called cells, which are labeled and can be nested. Computations carry computational meaning as special nested list structures sequentializing computational tasks, such as fragments of program. Computations extend the original language abstract syntax. K (rewrite) rules make it explicit which parts of the term they read-only, write-only, read-write, or do not care about. This makes K suitable for defining truly concurrent languages even in the presence of sharing. Computations are like any other terms in a rewriting environment: they can be matched, moved from one place to another, modified, or deleted. This makes K suitable for defining control-intensive features such as abrupt termination, exceptions or call/cc.\\ 
- 
-  * License: GPLv2\\ 
-  * Web site: http://k-framework.org 
 
formal_models_environments.1327747546.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ó