# Différences

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

formal_models_environments [Le 20/12/2012 à 16:26] david_mentre Ajout de SAL |
— (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/\\ | ||

- | |||

- | ==== 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\\ | ||

- | |||

- | \\ | ||

- | ==== Why3 ==== | ||

- | \\ | ||

- | [[why3|Why3]] is the next generation of the Why software verification platform. [[why3|Why3]] clearly separates the purely logical specification part from generation of verification conditions for programs. It features a rich library of proof task transformations that can be chained to produce a suitable input for a large set of theorem provers, including SMT solvers, TPTP provers, as well as interactive proof assistants.\\ | ||

- | |||

- | Supported provers: [[alt_-_ergo|Alt-Ergo]], Z3, CVC3, Yices 1, Simplify, Gappa, Coq\\ | ||

- | |||

- | * License: GNU GPL\\ | ||

- | * Web site: http://why3.lri.fr/\\ | ||

- | * Debian packages: why (for releases 2.x)\\ | ||

- | |||

- | \\ | ||

- | ==== Focal ==== | ||

- | \\ | ||

- | Focal (formerly known as %%FoC%%) is a language for software-proof codesign. In Focal, code, specifications, and proofs are developped together in the same source files, using a novel object-oriented module system. The compiler analyses the dependencies in order to ensure the consistency of the source, then translates the code to Objective Caml, and the proofs to Coq.\\ | ||

- | |||

- | * License: BSD like\\ | ||

- | * Web site: http://modulogic.inria.fr/focal/download/\\ | ||

- | |||

- | ==== FoCaLize ==== | ||

- | \\ | ||

- | The %%FoCaLize%%development effort started in 2006: it was clearly a continuation of the %%Foc%%and Focal efforts. The new system was rewritten from scratch. A new language and syntax was designed and carefully implemented, with in mind ease of use, expressivity, and programmer friendyness. The addition of powerful data structure definitions together with the corresponding pattern matching facility, lead to new expressing power.\\ | ||

- | |||

- | The Zenon automatic theorem prover was also integrated in the compiler and natively interfaced within the %%FoCaLize%%language. New developments for recursive functions support is on the way (in particular for termination proofs).\\ | ||

- | |||

- | A formal specification can be built by declaring names of functions and values and introducing properties. Then, design and implementation can incrementally be done by adding definitions of functions and proving that the implementation meets the specification or design requirements. Thus, developing in %%FoCaLize%%is a kind of refinement process from formal model to design and code, completely done within %%FoCaLize%%. Taking the global development in consideration within the same environment brings some conciseness, helps documentation and reviewing. Thus a %%FoCaLize%%development is organised as a hierarchy that may have several roots. The upper levels of the hierarchy are built along the specification stage while the lower ones correspond to implementation and each node of the hierarchy corresponds to a progress toward a complete implementation.\\ | ||

- | |||

- | The %%FoCaLize%%system provides means for the developers to formally express their specifications and to go step by step (in an incremental approach) to design and implementation while proving that such an implementation meets its specification or design requirements. The %%FoCaLize%%language offers high level mechanisms such as inheritance, late binding, redefinition, parametrization, etc. Confidence in proofs submitted by developers or automatically done relies on formal proof verification. %%FoCaLize%%also provides some automation of documentation production and management.\\ | ||

- | |||

- | * License: BSD like\\ | ||

- | * Web site: http://focalize.inria.fr\\ | ||

- | |||

- | \\ | ||

- | ==== Boogie ==== | ||

- | \\ | ||

- | Boogie is a program verification system that produces verification conditions for programs written in an intermediate language (also named Boogie). The intermediate language is easy to target from source languages such as Spec#, C#, or even C.\\ | ||

- | |||

- | * License: Microsoft Public License (Ms-PL)\\ | ||

- | * Web site: http://boogie.codeplex.com/ | ||

- | |||

- | ==== Rodin environment for Event B ==== | ||

- | |||

- | Event-B is a formal method for system-level modelling and analysis. Key features of Event-B are the use of set theory as a modelling notation, the use of refinement to represent systems at different abstraction levels and the use of mathematical proof to verify consistency between refinement levels. | ||

- | |||

- | The Rodin Platform is an Eclipse-based IDE for Event-B that provides effective support for refinement and mathematical proof. The platform is open source, contributes to the Eclipse framework and is further extendable with plugins. | ||

- | |||

- | * License: Eclipse Public License | ||

- | * Web site: http://www.event-b.org/ | ||

- | |||

- | ==== ProR ==== | ||

- | |||

- | ProR is a tool for requirements engineering that supports the ReqIF 1.0.1 Standard natively. It is part of the Eclipse RMF project and is built for extensibility. ProR is the result of the European Union FP7 Research Project Deploy, where it is used to provide traceability between requirements and formal models. | ||

- | |||

- | * License: Eclipse Public License | ||

- | * Web site: http://www.eclipse.org/rmf/pror/ | ||

- | |||

- | ==== SAL ==== | ||

- | |||

- | To become practical for assurance, automated formal methods must be made more scalable, automatic, and cost-effective. Such an increase in scope, scale, automation, and utility can be derived from an emphasis on a systematic separation of concerns during verification. SAL (Symbolic Analysis Laboratory) attempts to address these issues. It is a framework for combining different tools to calculate properties of concurrent systems. | ||

- | |||

- | The heart of SAL is a language, developed in collaboration with Stanford and Berkeley, for specifying concurrent systems in a compositional way. It is supported by a tool suite that includes state of the art symbolic (BDD-based) and bounded (SAT-based) model checkers, an experimental "Witness" model checker, and a unique "infinite" bounded model checker based on SMT solving. Auxiliary tools include a simulator, deadlock checker and an automated test generator. | ||

- | |||

- | * License: GNU GPL | ||

- | * Web site: http://sal.csl.sri.com/ | ||