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

free_software_for_formal_verification [Le 28/01/2012 à 11:44]
DavidMentre modification
— (Version actuelle)
Ligne 1: Ligne 1:
-====== Free software tools for formal verification of computer programs ====== 
-\\ 
-by  [[david_mentre|David Mentré]] <dmentre @ linux-france.org>\\ 
  
-//Version 2.0- 2012-01-28//\\ 
- 
-We are now living in the XXIst century. We should no longer make software as in the sixties or seventies, with a few tests. We are now able to make software without **any** bugs (well, without most of them, see below). This is possible using specialised tools called //formal tools//. Such tools are able to match a computer program against a specification, i.e. a formal description of the expected behaviour of the program. If the  specification is correct and the formal verification can be done, then the program is guaranteed to be bug free. Of course, this is the ideal case and we are far from guaranteed bug free programs in the real world. But, as developer of free software, we should try to be as close as possible of this goal. As a first step, I list here free software tools that can help verification of computer programs.\\ 
- 
-Note: David A. Wheeler as made a lengthy paper on [[http://www.dwheeler.com/essays/high-assurance-floss.html|High Assurance (for Security or Safety) and [[free_-_libre|Free-Libre]] / Open Source Software (FLOSS)... with Lots on Formal Methods]]. You should read it if you are interested in the subject!\\ 
- 
-[[sub_-pages|Sub-pages]] :\\ 
-    *  [[smtsolvers|SMT Solvers]]\\ 
-    *  [[proof_assistants|Proof assistants]]\\ 
-    *  [[model_checkers|Model checkers]]\\ 
-    *  [[program_dev_check_environments|Environments to develop and check programs]]\\ 
-    *  [[formal_models_environments|Environments to make and check formal models]]\\ 
- 
-===== 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/\\ 
- 
-===== Conclusion ===== 
-\\ 
-It remains to test all those programs. A hard task that is not yet done. 
 
free_software_for_formal_verification.1327747465.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ó