Ceci est une ancienne révision du document !


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.

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.

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.

[[proof_power|ProofPower]]


ProofPoweris 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 ProofPowerdeveloper kit, mainly comprising SLRP, a parser generator for Standard ML.
  • PPTex * The ProofPowerinterface to TeXand 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 ProofPowerpackages except PPDaz are free, open-source, software made available under the terms of the GNU General Public License.

ProofPowerhas 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 ProofPowerto Lemma 1 Ltd who now maintain this web site and support and distribute the software.


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.

 
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ó