(RAISE links) Tag: Source edit |
|||
(30 intermediate revisions by 17 users not shown) | |||
Line 9: | Line 9: | ||
Please update this page or add a new page if you know of relevant online information not included here or would like to maintain information on a particular topic. |
Please update this page or add a new page if you know of relevant online information not included here or would like to maintain information on a particular topic. |
||
− | Use the [ |
+ | Use the [http://groups.google.com/group/comp.specification.misc ''comp.specification.misc''] newsgroup, for general formal methods queries. Please link to [http://formalmethods.wikia.com/ <tt>http://formalmethods.wikia.com</tt>] if you create a permanent hyperlink to this website. |
In case of problems, please contact [[Jonathan Bowen]]. |
In case of problems, please contact [[Jonathan Bowen]]. |
||
Line 43: | Line 43: | ||
[[Image:star11t.gif|*]] ''This space will be used to indicate selected new entries and developments in these [http://dictionary.reference.com/search?q=formal+methods formal methods] pages.'' |
[[Image:star11t.gif|*]] ''This space will be used to indicate selected new entries and developments in these [http://dictionary.reference.com/search?q=formal+methods formal methods] pages.'' |
||
+ | <!-- [[Image:new.gif|!]] --> |
||
⚫ | |||
+ | * [http://scholar.google.co.uk/citations?view_op=search_authors&mauthors=label%3Aformal_methods Formal Methods] authors on {{wp|Google Scholar}}. (30 November 2011) |
||
+ | <!-- * [http://academic.research.microsoft.com/Keyword/14916/formal-method Formal Methods] on {{wp|Microsoft Academic Search}}. (29 November 2011) -- no longer working --> |
||
⚫ | |||
* [http://en.wikipedia.org/wiki/Category:Formal_methods Formal methods] entries in the [http://en.wikipedia.org/ Wikipedia] encyclopedia (30 October 2005) |
* [http://en.wikipedia.org/wiki/Category:Formal_methods Formal methods] entries in the [http://en.wikipedia.org/ Wikipedia] encyclopedia (30 October 2005) |
||
− | * The preferred and stable URL for the Virtual Library formal methods pages is now [http://vl.fmnet.info/ http://vl.fmnet.info] (30 November 2004) |
+ | * The preferred and stable URL for the Virtual Library formal methods pages is now [http://vl.fmnet.info/ http://vl.fmnet.info]. (30 November 2004) |
* Checked and updated main links to formal methods. (22 April 2001) |
* Checked and updated main links to formal methods. (22 April 2001) |
||
* Moved to the [http://www.cafm.lsbu.ac.uk/ Centre for Applied Formal Methods], [http://www.lsbu.ac.uk/ {{wp|London South Bank University}}. <!-- Note in particular that [[whos-who/search.html| searching]] now works again. --> (13 January 2001) |
* Moved to the [http://www.cafm.lsbu.ac.uk/ Centre for Applied Formal Methods], [http://www.lsbu.ac.uk/ {{wp|London South Bank University}}. <!-- Note in particular that [[whos-who/search.html| searching]] now works again. --> (13 January 2001) |
||
− | * New [http://www.iist.unu.edu/dc/ Duration Calculus] and [http://www.iist.unu.edu/raise/ RAISE] pages. (31 July 1999 / 17 August 1999) |
+ | <!-- * New [http://www.iist.unu.edu/dc/ Duration Calculus] and [http://www.iist.unu.edu/raise/ RAISE] pages. (31 July 1999 / 17 August 1999) --> |
* New [http://www.cs.indiana.edu/formal-methods-education/ education resources] section by [http://www.cs.rice.edu/~kfisler/ Kathi Fisler] added. (23 February 1999) |
* New [http://www.cs.indiana.edu/formal-methods-education/ education resources] section by [http://www.cs.rice.edu/~kfisler/ Kathi Fisler] added. (23 February 1999) |
||
* Search for newsgroup articles on [http://groups.google.com/groups?q=formal+methods&num=50&scoring=d formal methods] in [http://groups.google.com/ Google Groups]. (19 December 1997) |
* Search for newsgroup articles on [http://groups.google.com/groups?q=formal+methods&num=50&scoring=d formal methods] in [http://groups.google.com/ Google Groups]. (19 December 1997) |
||
Line 58: | Line 61: | ||
* [http://www.ora.on.ca/eves.html EVES] and [http://www.ora.on.ca/z-eves/ Z/EVES] are now available for on-line [http://www.ora.on.ca/distribution.html distribution]. (25 June 1996) |
* [http://www.ora.on.ca/eves.html EVES] and [http://www.ora.on.ca/z-eves/ Z/EVES] are now available for on-line [http://www.ora.on.ca/distribution.html distribution]. (25 June 1996) |
||
* [http://www.informatik.uni-kiel.de/~procos/dag9523/dag9523.html The Steam Boiler Control Specification Problem] by J.-R. Abrial, E. Börger and H. Langmaack. A comparative case study for different formal techniques. Published as [http://www.springer.de/catalog/html-files/deutsch/comp/3540619291.html LNCS 1165]. (2 August 1995) |
* [http://www.informatik.uni-kiel.de/~procos/dag9523/dag9523.html The Steam Boiler Control Specification Problem] by J.-R. Abrial, E. Börger and H. Langmaack. A comparative case study for different formal techniques. Published as [http://www.springer.de/catalog/html-files/deutsch/comp/3540619291.html LNCS 1165]. (2 August 1995) |
||
− | * [ |
+ | * [http://groups.google.com/group/comp.specification.misc ''Comp.specification.misc''] newsgroup. (12 July 1995) |
* [http://www.daimi.au.dk/PetriNets/ Petri Nets] graphical notation. (11 April 1995) |
* [http://www.daimi.au.dk/PetriNets/ Petri Nets] graphical notation. (11 April 1995) |
||
* [[WIFT95|Tools demonstration information]] for [http://www.cse.fau.edu/WIFT/ WIFT95] workshop. (6 April 1995) |
* [[WIFT95|Tools demonstration information]] for [http://www.cse.fau.edu/WIFT/ WIFT95] workshop. (6 April 1995) |
||
− | * A new [ |
+ | * A new [http://wwwtios.cs.utwente.nl/lotos/ LOTOS] page. (16 February 1995) |
* Information on [[RAISE]] language and tools. (19 January 1995, updated 17 August 1999) |
* Information on [[RAISE]] language and tools. (19 January 1995, updated 17 August 1999) |
||
* A new section on the [[B-Method]] has been added. (6 January 1995) |
* A new section on the [[B-Method]] has been added. (6 January 1995) |
||
Line 71: | Line 74: | ||
# [[Image:star11t.gif|*]] [http://www.eecs.umich.edu/gasm/ Abstract State Machines] ([[ASM]]). Formerly known as ''[[Evolving Algebras]]''. |
# [[Image:star11t.gif|*]] [http://www.eecs.umich.edu/gasm/ Abstract State Machines] ([[ASM]]). Formerly known as ''[[Evolving Algebras]]''. |
||
# [http://www.cs.utexas.edu/users/moore/acl2/ ACL2] (A Computational Logic for Applicative Common Lisp) theorem prover, a successor to the [[Nqthm]] [[Boyer-Moore theorem prover]]. |
# [http://www.cs.utexas.edu/users/moore/acl2/ ACL2] (A Computational Logic for Applicative Common Lisp) theorem prover, a successor to the [[Nqthm]] [[Boyer-Moore theorem prover]]. |
||
− | # [http://www.cis.upenn.edu/~rtg/formalismdesc.html ACSR] (Algebra of Communicating Shared Resources) and [http://www.cis.upenn.edu/~rtg/formalismdesc.html#GCSR |
+ | # [http://www.cis.upenn.edu/~rtg/formalismdesc.html ACSR] (Algebra of Communicating Shared Resources) and [http://www.cis.upenn.edu/~rtg/formalismdesc.html#GCSR Graphical Communicating Shared Resources] (GCSR), a formal language for the specification, refinement, and analysis of real-time systems. See the tools [http://www.cis.upenn.edu/~lee/duncan/versa.html VERSA] (Verification Execution and Rewrite System for ACSR) and [http://www.cis.upenn.edu/~lee/paragon.html PARAGON] for visual specification and verification of real-time systems. |
− | # [http://www.brics.dk/Projects/AS/ |
+ | # [http://www.brics.dk/Projects/AS/ Action Semantics], a framework for specifying formal semantics of programming languages. |
# [http://www.abo.fi/~Kaisa.Sere/distributed.html Action systems] for reasoning about distributed systems. |
# [http://www.abo.fi/~Kaisa.Sere/distributed.html Action systems] for reasoning about distributed systems. |
||
+ | # [http://www.absint.com/ait/ aiT WCET Analyzer], an abstract interpretation based static analyzer that computes safe upper bounds for the worst-case execution time of tasks. |
||
− | # [[Image:star11t.gif|*]] [http://alloy.mit.edu/ Alloy Analyzer], an object modelling notation that is compatible with development approaches such as [[UML]], Catalysis, Fusion, OMT and Syntropy, strongly influenced by the [[Z notation|Z specification language]]. See [http://groups.yahoo.com/group/alloy-discuss/ |
+ | # [[Image:star11t.gif|*]] [http://alloy.mit.edu/ Alloy Analyzer], an object modelling notation that is compatible with development approaches such as [[UML]], Catalysis, Fusion, OMT and Syntropy, strongly influenced by the [[Z notation|Z specification language]]. See [http://groups.yahoo.com/group/alloy-discuss/ Alloy discussion group]. |
⚫ | |||
− | # [http://www.cse.ogi.edu/~sheard/adl.html |
+ | # [http://www.cse.ogi.edu/~sheard/adl.html Algebraic Design Language], a higher-order software specification language. |
# [http://www-verimag.imag.fr/SYNCHRONE/argonaute-english.html Argos], an imperative synchronous language with verification support. |
# [http://www-verimag.imag.fr/SYNCHRONE/argonaute-english.html Argos], an imperative synchronous language with verification support. |
||
# [http://adl.opengroup.org/ Assertion Definition Language] (ADL), a specification based testing toolset. |
# [http://adl.opengroup.org/ Assertion Definition Language] (ADL), a specification based testing toolset. |
||
+ | # [http://www.absint.com/astree/ Astrée], an abstract interpretation based static analyzer that proves the absence of runtime errors in C programs. |
||
⚫ | |||
# [http://sprout.stanford.edu/dill/bdd.html BDDs] (Binary Decision Diagrams) for finite-state verification problems. |
# [http://sprout.stanford.edu/dill/bdd.html BDDs] (Binary Decision Diagrams) for finite-state verification problems. |
||
# [[Image:star11t.gif|*]] [[B-Method]], including the B-Tool and B-Toolkit. |
# [[Image:star11t.gif|*]] [[B-Method]], including the B-Tool and B-Toolkit. |
||
# [http://www.cs.utexas.edu/users/moore/best-ideas/nqthm/ Boyer-Moore theorem prover] (a forerunner of [[Nqthm]] and [[ACL2]]). Available via [[Logic programming#IFS| ICOT Free Software]] for use under Unix at [ftp://ftp.icot.or.jp/ifs/solver-prover/unix/bmtp.tar.Z ICOT] (Japan). |
# [http://www.cs.utexas.edu/users/moore/best-ideas/nqthm/ Boyer-Moore theorem prover] (a forerunner of [[Nqthm]] and [[ACL2]]). Available via [[Logic programming#IFS| ICOT Free Software]] for use under Unix at [ftp://ftp.icot.or.jp/ifs/solver-prover/unix/bmtp.tar.Z ICOT] (Japan). |
||
+ | # [[Image:star11t.gif|*]] [http://cadp.inria.fr CADP]: a widespread toolbox for the Construction and Analysis of Distributed Processes, developed at INRIA Grenoble |
||
# [[Image:star11t.gif|*]] [http://www.cofi.info/CASL.html CASL]: Common Algebraic Specification Language, for algebraic specification and development, from [[CoFI]], the Common Framework Initiative. |
# [[Image:star11t.gif|*]] [http://www.cofi.info/CASL.html CASL]: Common Algebraic Specification Language, for algebraic specification and development, from [[CoFI]], the Common Framework Initiative. |
||
# [[Image:star11t.gif|*]] [http://www.ldl.jaist.ac.jp/cafeobj/ CafeOBJ], an algebraic specification and programming language. A successor of [[OBJ]]. |
# [[Image:star11t.gif|*]] [http://www.ldl.jaist.ac.jp/cafeobj/ CafeOBJ], an algebraic specification and programming language. A successor of [[OBJ]]. |
||
# [[Image:star11t.gif|*]] [[CCS]] (Calculus of Communicating Systems). A process algebra for concurrent systems. |
# [[Image:star11t.gif|*]] [[CCS]] (Calculus of Communicating Systems). A process algebra for concurrent systems. |
||
− | # [http://www.cis.unisa.edu.au/acrc-doc/circal/circal_system.html Circal] (CIRcuit CALculus) System supporting a process algebra which may be used to rigorously describe, verify and simulate concurrent systems. See [http://www.cis.unisa.edu.au/acrc/cs/fsv/dhv/circal:software |
+ | # [http://www.cis.unisa.edu.au/acrc-doc/circal/circal_system.html Circal] (CIRcuit CALculus) System supporting a process algebra which may be used to rigorously describe, verify and simulate concurrent systems. See [http://www.cis.unisa.edu.au/acrc/cs/fsv/dhv/circal:software software]. |
# [http://www.dcs.gla.ac.uk/~boulton/claret/ CLaReT]: The Computer Language Reasoning Tool. |
# [http://www.dcs.gla.ac.uk/~boulton/claret/ CLaReT]: The Computer Language Reasoning Tool. |
||
# [http://www.phil.ruu.nl/~keesm/NSD.html COLD] (Common Object-oriented Language for Design), a wide-spectrum specification language. |
# [http://www.phil.ruu.nl/~keesm/NSD.html COLD] (Common Object-oriented Language for Design), a wide-spectrum specification language. |
||
Line 93: | Line 99: | ||
# [[Image:star11t.gif|*]] [[CSP]] (Communicating Sequential Processes) including the [http://www.formal.demon.co.uk/FDR2.html FDR2] (Failures-Divergence Refinement) tool. |
# [[Image:star11t.gif|*]] [[CSP]] (Communicating Sequential Processes) including the [http://www.formal.demon.co.uk/FDR2.html FDR2] (Failures-Divergence Refinement) tool. |
||
# [http://www.dcs.ed.ac.uk/home/cwb/ CWB] [[Concurrency Factory]] and [http://www.csc.ncsu.edu/eos/users/r/rance/WWW/cwb-nc.html CWB-NC] (The Concurrency Workbench of North Carolina), which includes a [[LOTOS]] interface, diagnostic information, etc. Note: The CWB and CWB-NC have a common ancestor, but are each under separate development. |
# [http://www.dcs.ed.ac.uk/home/cwb/ CWB] [[Concurrency Factory]] and [http://www.csc.ncsu.edu/eos/users/r/rance/WWW/cwb-nc.html CWB-NC] (The Concurrency Workbench of North Carolina), which includes a [[LOTOS]] interface, diagnostic information, etc. Note: The CWB and CWB-NC have a common ancestor, but are each under separate development. |
||
+ | # [http://symbolaris.com/logic/dL.html dL -- differential dynamic logic] for hybrid systems verification. |
||
# [http://disco.cs.tut.fi/ DisCo] specification method for reactive systems including an [http://disco.cs.tut.fi/animation/Animation.html animation tool], Finland. |
# [http://disco.cs.tut.fi/ DisCo] specification method for reactive systems including an [http://disco.cs.tut.fi/animation/Animation.html animation tool], Finland. |
||
− | # [[Image:star11t.gif|*]][http://www.iist.unu.edu/dc/ |
+ | # [[Image:star11t.gif|*]][http://www.iist.unu.edu/dc/ Duration Calculus] (DC), an interval logic for real-time systems. |
# [[Image:star11t.gif|*]][http://secure.ucd.ie/products/opensource/ESCJava2/ ESC/Java2] Extended Static Checker for [http://java.sun.com/ Java] tool, using program verification technology. See also [[JML]]. |
# [[Image:star11t.gif|*]][http://secure.ucd.ie/products/opensource/ESCJava2/ ESC/Java2] Extended Static Checker for [http://java.sun.com/ Java] tool, using program verification technology. See also [[JML]]. |
||
+ | # [[Image:star11t.gif|*]] [http://www.eschertech.com/products/ecv.php Escher C Verifier], a tool for formal verification of embedded software written in MISRA-C. |
||
− | # [http://www.estelle.org/ |
+ | # [http://www.estelle.org/ Estelle] Formal Description Technique (IS 9074). See also [http://www-lor.int-evry.fr/edt/ EDT] (Estelle Development Toolset). |
− | # [[Image:star11t.gif|*]] [http://www-sop.inria.fr/esterel.org/ |
+ | # [[Image:star11t.gif|*]] [http://www-sop.inria.fr/esterel.org/ Esterel] language and tools for synchronous reactive systems. |
− | # [http://www.ora.on.ca/eves.html EVES] tool, based on ZF set theory, from [http://www.ora.on.ca/ ORA], Canada. See also [http://www.ora.on.ca/z-eves/welcome.html |
+ | # [http://www.ora.on.ca/eves.html EVES] tool, based on ZF set theory, from [http://www.ora.on.ca/ ORA], Canada. See also [http://www.ora.on.ca/z-eves/welcome.html Z/EVES] which provides a [[Z notation]] front-end to EVES. |
# [http://homepages.inf.ed.ac.uk/dts/eml/ Extended ML] framework for the specification and [http://homepages.inf.ed.ac.uk/dts/alf/ formal development] of modular Standard ML programs. |
# [http://homepages.inf.ed.ac.uk/dts/eml/ Extended ML] framework for the specification and [http://homepages.inf.ed.ac.uk/dts/alf/ formal development] of modular Standard ML programs. |
||
# [http://www.cse.dmu.ac.uk/~mward/fermat.html FermaT program transformation system]. See also [http://www.dur.ac.uk/~dcs0mpw/fermat.html here]. |
# [http://www.cse.dmu.ac.uk/~mward/fermat.html FermaT program transformation system]. See also [http://www.dur.ac.uk/~dcs0mpw/fermat.html here]. |
||
− | # [http://www.cadence.com/datasheets/formalcheck.html |
+ | # [http://www.cadence.com/datasheets/formalcheck.html FormalCheck] model checker tool for verifying the functionality of digital hardware designs in Verilog or VHDL, based on the COSPAN [[model checker]]. |
# [[Image:star11t.gif|*]] [[HOL]] mechanical theorem proving system, based on Higher Order Logic. |
# [[Image:star11t.gif|*]] [[HOL]] mechanical theorem proving system, based on Higher Order Logic. |
||
− | # [http://www.eecs.berkeley.edu/~tah/HyTech/ |
+ | # [http://www.eecs.berkeley.edu/~tah/HyTech/ HyTech] (The HYbrid TECHnology Tool), an automatic tool for the analysis of embedded systems which computes the condition under which a linear hybrid system satisfies a temporal-logic requirement. |
− | # [[Image:star11t.gif|*]] [http://imps.mcmaster.ca/ |
+ | # [[Image:star11t.gif|*]] [http://imps.mcmaster.ca/ IMPS], an Interactive Mathematical Proof System intended to provide mechanical support for traditional mathematical techniques and styles of practice. |
− | # [[Image:star11t.gif|*]] [http://www.cse.dmu.ac.uk/~cau/itlhomepage/ Interval Temporal Logic] (ITL). See also [http://liinwww.ira.uka.de/waisbib?database=local/bibliography&sortmode=date&maxhits=200&convert=bibtex&ti=Interval and Temporal and Logic |
+ | # [[Image:star11t.gif|*]] [http://www.cse.dmu.ac.uk/~cau/itlhomepage/ Interval Temporal Logic] (ITL). See also [http://liinwww.ira.uka.de/waisbib?database=local/bibliography&sortmode=date&maxhits=200&convert=bibtex&ti=Interval and Temporal and Logic publications]. |
# [[Image:star11t.gif|*]] [http://www.cl.cam.ac.uk/Research/HVG/Isabelle/ Isabelle], a generic theorem prover, supporting higher-order logic, ZF set theory, etc. |
# [[Image:star11t.gif|*]] [http://www.cl.cam.ac.uk/Research/HVG/Isabelle/ Isabelle], a generic theorem prover, supporting higher-order logic, ZF set theory, etc. |
||
− | # [http://users.comlab.ox.ac.uk/bernard.sufrin/jape.html |
+ | # [http://users.comlab.ox.ac.uk/bernard.sufrin/jape.html Jape] (Just Another Proof Editor). A framework for building interactive proof editors. |
− | # [[Image:star11t.gif|*]] [http://www.jmlspecs.org/ |
+ | # [[Image:star11t.gif|*]] [http://www.jmlspecs.org/ JML] (Java Modeling Language), a behavioral interface specification language for [http://java.sun.com/ Java]. See also [[ESC/Java2]]. |
− | # [http://www.key-project.org |
+ | # [http://www.key-project.org KeY] An automatic and interactive, verification and test generation tool for Java Card. |
− | # [http://symbolaris.com/info/KeYmaera.html |
+ | # [http://symbolaris.com/info/KeYmaera.html KeYmaera] A Hybrid Theorem Prover for Hybrid Systems. |
− | # [http://i11www.ira.uka.de/~kiv/ |
+ | # [http://i11www.ira.uka.de/~kiv/ KIV] (Karlsruhe Interactive Verifier). A tool for the development of correct software using stepwise refinement. |
− | # [http://www.imag.fr/VERIMAG/TEMPORISE/kronos/index-english.html |
+ | # [http://www.imag.fr/VERIMAG/TEMPORISE/kronos/index-english.html Kronos], a verification tool for safety and liveness properties of real-time systems. Uses timed automata, TCTL (an extension of temporal logic) and model-checking. |
− | # [[Image:star11t.gif|*]] [http://www.sds.lcs.mit.edu/spd/larch/ |
+ | # [[Image:star11t.gif|*]] [http://www.sds.lcs.mit.edu/spd/larch/ Larch] family of languages and tools supporting a two-tiered definitional style of specification. See especially [http://www.sds.lcs.mit.edu/spd/larch/LP/overview.html LP], the Larch Prover. |
− | # [http://i12www.ira.uka.de/leantap/ |
+ | # [http://i12www.ira.uka.de/leantap/ LeanTAP], a tableau-based deduction theorem prover for classical first-order logic. |
− | # [http://www.dcs.ed.ac.uk/home/lego/ |
+ | # [http://www.dcs.ed.ac.uk/home/lego/ LEGO] proof assistant. |
− | # [http://www.leoprover.org |
+ | # [http://www.leoprover.org Leo-II] resolution-based automated theorem prover for Higher-Order Logic |
− | # [[Image:star11t.gif|*]] [http://www.cs.stir.ac.uk/~kjt/research/well/ |
+ | # [[Image:star11t.gif|*]] [http://www.cs.stir.ac.uk/~kjt/research/well/ LOTOS] (Language of Temporal Ordering Specifications). |
− | # [http://www.info.unicaen.fr/lpv/ |
+ | # [http://www.info.unicaen.fr/lpv/ LPV] Linear Programming based software Validation technology, including proofs and testing. |
− | # [http://www-verimag.imag.fr/SYNCHRONE/lustre-english.html |
+ | # [http://www-verimag.imag.fr/SYNCHRONE/lustre-english.html Lustre] synchronous declarative language for programming reactive systems, including verification. |
− | # [http://www.tagroup.co.uk/malpas.htm |
+ | # [http://www.tagroup.co.uk/malpas.htm MALPAS] static analysis tool-set. |
− | # [http://www.dur.ac.uk/CSM/projects/ma/ |
+ | # [http://www.dur.ac.uk/CSM/projects/ma/ Maintainer's Assistant], a tool for reverse engineering and re-engineering code using formal methods. |
− | # [http://www.cs.nott.ac.uk/~rcb/mathspad/ |
+ | # [http://www.cs.nott.ac.uk/~rcb/mathspad/ MathSpad] structure editor, especially for mathematical calculations. |
− | # [http://maude.cs.uiuc.edu/ |
+ | # [http://maude.cs.uiuc.edu/ Maude] system for equational and rewriting logic specification and programming. Influenced by [[OBJ3]]. |
− | # [http://www.inria.fr/meije/meijetools.html |
+ | # [http://www.inria.fr/meije/meijetools.html Meije] tools for the verification of concurrent programs. Includes ATG, a graphical editor/visualizer. |
# [http://www.cwi.nl/~mcrl/ μCRL] (micro CRL), process algebraic language for communicating processes with data. |
# [http://www.cwi.nl/~mcrl/ μCRL] (micro CRL), process algebraic language for communicating processes with data. |
||
# [http://www.mcrl2.org/ mCRL2] a toolset for a process algebraic language and a modal logic with data and time. Successor of μCRL. |
# [http://www.mcrl2.org/ mCRL2] a toolset for a process algebraic language and a modal logic with data and time. Successor of μCRL. |
||
− | # [http://www.mizar.org/system/ |
+ | # [http://www.mizar.org/system/ Mizar System], a long-term effort aimed at developing software to support a working mathematician in preparing papers. See also [http://web.cs.ualberta.ca/~piotr/Mizar/ here]. |
# [[Image:star11t.gif|*]] [http://www.cs.cmu.edu/~modelcheck/ Model checking] at CMU, a method for formally verifying finite-state concurrent systems. [http://www.cs.cmu.edu/~modelcheck/code.html Available packages] include: |
# [[Image:star11t.gif|*]] [http://www.cs.cmu.edu/~modelcheck/ Model checking] at CMU, a method for formally verifying finite-state concurrent systems. [http://www.cs.cmu.edu/~modelcheck/code.html Available packages] include: |
||
#* [http://www.cs.cmu.edu/~modelcheck/bdd.html BDD library] with extensions for sequential verification. |
#* [http://www.cs.cmu.edu/~modelcheck/bdd.html BDD library] with extensions for sequential verification. |
||
#* [http://www.cs.cmu.edu/~deharbe/project.html CV], a VHDL model checker. |
#* [http://www.cs.cmu.edu/~deharbe/project.html CV], a VHDL model checker. |
||
#* [http://www.cs.cmu.edu/~modelcheck/csml.html CSML and MCB], a language for compositional description of finite state machines and a (non-symbolic) model checker for CTL. |
#* [http://www.cs.cmu.edu/~modelcheck/csml.html CSML and MCB], a language for compositional description of finite state machines and a (non-symbolic) model checker for CTL. |
||
− | #* [http://www.cs.cmu.edu/~modelcheck/smv.html SMV] (Symbolic Model Verifier) model checker for finite-state systems, using the specification language CTL (Computation Tree Logic), a propositional branching-time temporal logic. See also [http://www.cs.cmu.edu/~modelcheck/wsmv.html |
+ | #* [http://www.cs.cmu.edu/~modelcheck/smv.html SMV] (Symbolic Model Verifier) model checker for finite-state systems, using the specification language CTL (Computation Tree Logic), a propositional branching-time temporal logic. See also [http://www.cs.cmu.edu/~modelcheck/wsmv.html Word-level SMV] for verifying arithmetic circuits efficiently. See also [[Image:star11t.gif|*]] [http://nusmv.irst.itc.it/ NuSMV], a new symbolic model checker. |
− | # [http://sprout.stanford.edu/dill/murphi.html |
+ | # [http://sprout.stanford.edu/dill/murphi.html Murphi] description language and verifier tool for finite-state verification of concurrent systems. |
− | # [[Image:star11t.gif|*]] [http://www.cs.utexas.edu/users/boyer/ftp/nqthm/ |
+ | # [[Image:star11t.gif|*]] [http://www.cs.utexas.edu/users/boyer/ftp/nqthm/ Nqthm] 1992, the latest [[Boyer-Moore theorem prover]]. Also [ftp://ftp.cs.utexas.edu/pub/boyer/nqthm/index.html accessible via FTP]. Includes the Pc-Nqthm interactive Proof-checker. |
# [[Image:star11t.gif|*]] [http://www.cs.cornell.edu/Info/Projects/NuPrl/ Nuprl] tool based on intuitionistic type theory. |
# [[Image:star11t.gif|*]] [http://www.cs.cornell.edu/Info/Projects/NuPrl/ Nuprl] tool based on intuitionistic type theory. |
||
# [[Image:star11t.gif|*]] [[OBJ]] family — [[OBJ3]], 2OBJ, [[CafeOBJ]], etc. Term rewriting and algebraic specification. |
# [[Image:star11t.gif|*]] [[OBJ]] family — [[OBJ3]], 2OBJ, [[CafeOBJ]], etc. Term rewriting and algebraic specification. |
||
− | # [http://www-3.ibm.com/software/awdtools/library/standards/ocl.html |
+ | # [http://www-3.ibm.com/software/awdtools/library/standards/ocl.html OCL] (Object Constraint Language), part of [[#UML| UML]]. |
# [http://www.mcs.anl.gov/home/mccune/ar/otter/ Otter], an automated deduction system. |
# [http://www.mcs.anl.gov/home/mccune/ar/otter/ Otter], an automated deduction system. |
||
− | # [http://www.dcs.ed.ac.uk/pepa/ |
+ | # [http://www.dcs.ed.ac.uk/pepa/ PEPA], a stochastic process algebra used for modelling systems composed of concurrently active components that co-operate and share work. |
− | # [[Image:star11t.gif|*]] [http://www.eschertech.com/products/ |
+ | # [[Image:star11t.gif|*]] [http://www.eschertech.com/products/ Perfect Developer] tool from [[Escher-Technologies|Escher Techologies Limited]]. |
− | # [[Image:star11t.gif|*]] [http://www.daimi.au.dk/PetriNets/ |
+ | # [[Image:star11t.gif|*]] [http://www.daimi.au.dk/PetriNets/ Petri Nets], a formal graphical notation for modelling systems with concurrency. See also [http://www.petrinets.org/ here]. |
− | # [[Image:star11t.gif|*]] [http://lampwww.epfl.ch/mobility/ |
+ | # [[Image:star11t.gif|*]] [http://lampwww.epfl.ch/mobility/ Pi-calculus]<nowiki>: calculi for mobile processes. See also the </nowiki>[http://www.it.uu.se/research/group/mobility/mwb Mobility Workbench] and a [http://liinwww.ira.uka.de/bibliography/Theory/pi.html searchable bibliography]. |
− | # [http://www.cs.man.ac.uk/fmethods/projects/pobl-development-method.html |
+ | # [http://www.cs.man.ac.uk/fmethods/projects/pobl-development-method.html Pobl]. A development method for concurrent object-based programs. |
# [http://www.lemma-one.demon.co.uk/ProofPower/ ProofPower] is a commercial tool, developed by [[ICL]], supporting development and checking of specifications and formal proofs in [[Higher Order Logic]] and/or [[Z]]. Support for Z uses a deep(ish) embedding of Z into HOL, but includes syntax and type checking customized for Z. |
# [http://www.lemma-one.demon.co.uk/ProofPower/ ProofPower] is a commercial tool, developed by [[ICL]], supporting development and checking of specifications and formal proofs in [[Higher Order Logic]] and/or [[Z]]. Support for Z uses a deep(ish) embedding of Z into HOL, but includes syntax and type checking customized for Z. |
||
− | # [http://www.prover.com/products_services/ |
+ | # [http://www.prover.com/products_services/ Prover Technology], commercial proof engines. |
# [[Image:star11t.gif|*]] [[PVS]] (Prototype Verification System) language and tool based on classical typed higher-order logic. |
# [[Image:star11t.gif|*]] [[PVS]] (Prototype Verification System) language and tool based on classical typed higher-order logic. |
||
− | # [[Image:star11t.gif|*]] [ |
+ | # [[Image:star11t.gif|*]] [[RAISE]] (Rigorous Approach to Industrial Software Engineering). Includes RSL (RAISE Specification Language). |
− | # [http://pavg.stanford.edu/rapide/ |
+ | # [http://pavg.stanford.edu/rapide/ Rapide] language and toolset, for building large-scale distributed multi-language systems. |
− | # [http://www.ecs.soton.ac.uk/~mjb/refcalc-tut/home.html |
+ | # [http://www.ecs.soton.ac.uk/~mjb/refcalc-tut/home.html Refinement Calculus], a formalisation of the stepwise refinement method of program construction. |
+ | # [http://www.risc.jku.at/research/formal/software/ProgramExplorer RISC ProgramExplorer], a computer-supported program reasoning environment for educational purposes. |
||
− | # [http://www.itd.nrl.navy.mil/ITD/5540/personnel/heitmeyer.html |
+ | # [http://www.itd.nrl.navy.mil/ITD/5540/personnel/heitmeyer.html SCR] (Software Cost Reduction), a tabular notation for specifying requirements and tools for creating and analyzing requirements specifications. |
− | # [[Image:star11t.gif|*]] [http://www.sdl-forum.org/ |
+ | # [[Image:star11t.gif|*]] [http://www.sdl-forum.org/ SDL] (Specification and Description Language) from the [http://www.sdl-forum.org/forum.html SDL Forum Society]. See also previous site [http://www.tdr.dk/public/SDL/ here]. |
− | # [http://www.irisa.fr/espresso/Polychrony/ |
+ | # [http://www.irisa.fr/espresso/Polychrony/ Signal/Polychrony] language and toolset for synchronous systems. See also the related [[Esterel]] and [[Lustre]]. |
− | # [[Image:star11t.gif|*]] [http://www.sparkada.com/ SPARK] secure subset of Ada, including the [http://www.sparkada.com/spade.html SPADE] static analysis toolset. |
||
− | # [[Image:star11t.gif|*]] [http:// |
+ | # [[Image:star11t.gif|*]] [http://www.altran-praxis.com/spark.aspx SPARK (now AltranPraxis)] secure subset of Ada, including the SPADE static analysis toolset. |
+ | # [[Image:star11t.gif|*]] [http://research.microsoft.com/specsharp/ Spec#], an extension of the [http://en.wikipedia.org/wiki/C_Sharp C#] programming language from [http://research.microsoft.com/ Microsoft Research] with specification features allowing static analysis using a program verifier. |
||
− | # [http://www.specware.org/ |
+ | # [http://www.specware.org/ Specware] automated software development system for stepwise refinement of provably correct code. See also [http://www.kestrel.edu/home/techtransfer.html technology transfer] information and publication from the [http://www.kestrel.edu/ Kestrel Institute]. |
− | # [[Image:star11t.gif|*]] [http://www.spinroot.com/ |
+ | # [[Image:star11t.gif|*]] [http://www.spinroot.com/ SPIN] is an automated verification tool ([[#MODELCHECK|model checker]]), using PROMELA (PROcess MEta LAnguage), a language loosely based on [[CSP]], for finite state systems, such as protocols or validation models of distributed systems, developed at [http://www.cs.bell-labs.com/cm/cs/what/formal_methods/ Bell Laboratories]. See also [http://goethe.ira.uka.de/~baldamus/p2b/ p2b], a translation utility. |
+ | # [http://www.absint.com/stackanalyzer/ StackAnalyzer], an abstract interpretation based static analyzer for computing the worst-case stack usage of tasks. |
||
# [http://www.flowgate.net/?lang=en&seccion=herramientas# StateSim] simulator for Statecharts models. Draw your models in Open Office Draw and the run your simulations from StateSim. |
# [http://www.flowgate.net/?lang=en&seccion=herramientas# StateSim] simulator for Statecharts models. Draw your models in Open Office Draw and the run your simulations from StateSim. |
||
− | # [http://statestep.com/ Statestep] finite state machine modelling with comprehensive elicitation of unusual scenarios. |
+ | # [http://statestep.com/ Statestep] finite state machine modelling with comprehensive elicitation of unusual scenarios (addressing "corner cases" or the feature interaction problem). |
# [http://www-step.stanford.edu/ STeP], the Stanford Temporal Prover. |
# [http://www-step.stanford.edu/ STeP], the Stanford Temporal Prover. |
||
− | # [http://w3.uqah.uquebec.ca/iglewski/public_html/TAM/ |
+ | # [http://w3.uqah.uquebec.ca/iglewski/public_html/TAM/ TAM'97] (Trace Assertion Method). A formal method for abstract specification of module interfaces. |
− | # [http://www.time-rover.com/TRindex.html |
+ | # [http://www.time-rover.com/TRindex.html Temporal-Rover] — formal specification and testing tool based on [http://www.time-rover.com/tl.html temporal logic]. |
− | # [ |
+ | # [[TLA]] (Temporal Logic of Actions), a logic for specifying and reasoning about concurrent and reactive systems. |
# [http://gtps.math.cmu.edu/tps.html TPS and ETPS], the Theorem Proving System and the Educational Theorem Proving System. |
# [http://gtps.math.cmu.edu/tps.html TPS and ETPS], the Theorem Proving System and the Educational Theorem Proving System. |
||
# [http://www.elet.polimi.it/res/TRIO/ TRIO] language and tools for real-time systems, based on temporal logic. |
# [http://www.elet.polimi.it/res/TRIO/ TRIO] language and tools for real-time systems, based on temporal logic. |
||
# [http://www.cs.yorku.ca/~stateclock/ TTM/RTTL] framework for real-time reactive systems. |
# [http://www.cs.yorku.ca/~stateclock/ TTM/RTTL] framework for real-time reactive systems. |
||
− | # [http://www.cs.utexas.edu/users/psp/welcome.html#unitysec |
+ | # [http://www.cs.utexas.edu/users/psp/welcome.html#unitysec UNITY], a programming notation and a logic to reason about parallel and distributed programs. |
# [http://www.docs.uu.se/docs/rtmv/uppaal/ UPPAAL] verification and validation tools for real-time systems. [[Model checking]] and simulation with a graphical interface. |
# [http://www.docs.uu.se/docs/rtmv/uppaal/ UPPAAL] verification and validation tools for real-time systems. [[Model checking]] and simulation with a graphical interface. |
||
+ | # [http://vcc.codeplex.com VCC], Microsoft Research - Verification of Concurrent C; a sound deductive verifier for C. |
||
# [http://www.bell-labs.com/projects/verisoft/ VeriSoft], Bell Laboratories, Lucent Technologies. A [[model checking]] tool for systematic software testing of concurrent/reactive/real-time systems. Automatically searches for coordination problems (deadlocks, etc.) and assertion violations. Supports C, C++, etc. |
# [http://www.bell-labs.com/projects/verisoft/ VeriSoft], Bell Laboratories, Lucent Technologies. A [[model checking]] tool for systematic software testing of concurrent/reactive/real-time systems. Automatically searches for coordination problems (deadlocks, etc.) and assertion violations. Supports C, C++, etc. |
||
# [[Image:star11t.gif|*]] [http://www.vdmportal.org/ VDM] ([[Vienna Development Method]]). See also [http://www.overturetool.org/ Overture toolset]. |
# [[Image:star11t.gif|*]] [http://www.vdmportal.org/ VDM] ([[Vienna Development Method]]). See also [http://www.overturetool.org/ Overture toolset]. |
||
# [http://www-cad.eecs.Berkeley.EDU/~vis/ VIS] (Verification Interacting with Synthesis), a system for formal verification, synthesis, and simulation of finite state systems, especially logic circuits. Includes a Verilog HDL front-end. |
# [http://www-cad.eecs.Berkeley.EDU/~vis/ VIS] (Verification Interacting with Synthesis), a system for formal verification, synthesis, and simulation of finite state systems, especially logic circuits. Includes a Verilog HDL front-end. |
||
# [http://www.x-machines.net/ X-machines], related to finite state machines. |
# [http://www.x-machines.net/ X-machines], related to finite state machines. |
||
− | # [[Image:star11t.gif|*]] [[Z notation]] for formal specification. |
+ | # [[Image:star11t.gif|*]] [[Z notation]] for formal specification and extensions eg. TCOZ (Timed Communicating Object Z) . |
See also: |
See also: |
||
− | * [[Image:star11t.gif|*]] [http://en.wikipedia.org/wiki/Formal_methods Formal methods] entry and [http://en.wikipedia.org/wiki/Category:Formal_methods |
+ | * [[Image:star11t.gif|*]] [http://en.wikipedia.org/wiki/Formal_methods Formal methods] entry and [http://en.wikipedia.org/wiki/Category:Formal_methods category] in the [http://en.wikipedia.org/ Wikipedia] free online encyclopedia. |
− | * [[Image:star11t.gif|*]] [http://www.fmeurope.org/ |
+ | * [[Image:star11t.gif|*]] [http://www.fmeurope.org/ Formal Methods Europe] (FME) HUB. |
− | * [[Image:star11t.gif|*]] [http://www.cs.indiana.edu/formal-methods-education/Tools/ |
+ | * [[Image:star11t.gif|*]] [http://www.cs.indiana.edu/formal-methods-education/Tools/ Formal Methods Education Resources: Tool Pages]. |
− | * [http://www.imag.fr/VERIMAG/VERIF/methodes-english.html |
+ | * [http://www.imag.fr/VERIMAG/VERIF/methodes-english.html Formal Verification Methods and Tools] from the [http://www.imag.fr/VERIMAG/index-english.html VERIMAG] [http://www.imag.fr/VERIMAG/ACTIVITIES/activites-english.html research group], France. |
<!-- * [[WIFT95|Tools demonstration information]] for WIFT'95 workshop. --> |
<!-- * [[WIFT95|Tools demonstration information]] for WIFT'95 workshop. --> |
||
* [http://gulliver.eu.org/ateliers/fv-tools/ Formal verification Tools] list from David Mentre, [http://gulliver.eu.org/ Association Gulliver]. |
* [http://gulliver.eu.org/ateliers/fv-tools/ Formal verification Tools] list from David Mentre, [http://gulliver.eu.org/ Association Gulliver]. |
||
Line 185: | Line 196: | ||
==Newsgroups and mailing lists== |
==Newsgroups and mailing lists== |
||
− | * [ |
+ | * [http://groups.google.com/group/comp.specification.misc ''Comp.specification.misc''] newsgroup including discussion of formal specification and methods, and other [http://groups.google.com/groups/dir?sel=usenet%3Dcomp.specification%2C& related newsgroups] (see [http://www.liszt.com/news/search.cgi?word=comp.specification ''comp.specification'' newsgroups] and [http://groups.google.com/groups/comp.specification.misc here] if you have news access problems): |
− | ** [ |
+ | ** [http://groups.google.com/group/comp.specification.larch ''Comp.specification.larch''] — more specific discussion on the [[Larch]], now an archive. |
− | ** [ |
+ | ** [http://groups.google.com/group/comp.specification.z ''Comp.specification.z''] — more specific discussion on the [[Z notation|Z and related notations]]. See monthly [http://www.faqs.org/faqs/z-faq/ FAQ message] (Frequently Asked Questions). |
− | * [ |
+ | * [http://groups.google.com/group/comp.software-eng ''Comp.software-eng''] — general discussion on software engineering, including formal aspects. See also the [http://www.qucis.queensu.ca/Software-Engineering/ ''comp.software-eng'' Software Engineering Archives] and [http://www.faqs.org/faqs/software-eng/ FAQ message information] especially [http://www.faqs.org/faqs/software-eng/part3/ formal specification]. |
− | * [ |
+ | * [http://groups.google.com/groups/news.announce.conferences ''News.announce.conferences''] — announcements of conferences including many specifically on [http://groups.google.com/groups?q=formal+methods&num=50&scoring=d formal methods] or with a formal methods content; e.g., see separate page on [[meetings]]. |
− | * [[Image:star11t.gif|*]] Search for newsgroup articles on [http://groups.google.com/groups?oi=djq&as_q=formal+methods |
+ | * [[Image:star11t.gif|*]] Search for newsgroup articles on [http://groups.google.com/groups?oi=djq&as_q=formal+methods formal methods] in [http://groups.google.com/ Google Groups]. |
− | * [[Image:star11t.gif|*]] [http://www.phoaks.com/phoaks2/newsgroups/comp/specification/nfr_index.html ''Comp.specification.*'' Frequently Mentioned Resources] from [http://www.phoaks.com/ People Helping One Another Know Stuff] (PHOAKS). A count of and link to URLs mentioned in newsgroup articles. See also [http://www.phoaks.com/cgi-bin/get-page?NEWSGROUP=comp.software-eng;QUERY_TYPE=urls-frequency;DISPLAY_RANGE=1-10;DISPLAY_TYPE=html_lofi ''comp.software-eng'' resources]. |
||
The following electronic mailing lists cover general issues concerning formal methods: |
The following electronic mailing lists cover general issues concerning formal methods: |
||
+ | * [http://www.jiscmail.ac.uk/lists/fmnet.html ProCoS mailing list]. [[FMnet]], maintained by [[Jonathan Bowen]]. |
||
− | * Educational issues relating to formal methods in computer science. Email [mailto:formal-methods-request@cs.uidaho.edu ''formal-methods-request@cs.uidaho.edu''] to join/leave the list and [mailto:formal-methods@cs.uidaho.edu ''formal-methods@cs.uidaho.edu''] to post to the list. |
||
− | * [http://www.jiscmail.ac.uk/lists/procos.html |
+ | * [http://www.jiscmail.ac.uk/lists/procos.html ProCoS mailing list]. [[Provably Correct Systems]], maintained by [[Jonathan Bowen]]. |
There are a significant number of mailing lists concerning individual formal methods. Please see the relevant pages for the formal methods of interest for details. |
There are a significant number of mailing lists concerning individual formal methods. Please see the relevant pages for the formal methods of interest for details. |
||
Line 204: | Line 214: | ||
See also information on: |
See also information on: |
||
⚫ | |||
⚫ | |||
⚫ | |||
⚫ | |||
− | * <!-- compulog/ --> [[Computational logic]] |
||
* [[Concurrent systems]] |
* [[Concurrent systems]] |
||
* [[Logic programming]] |
* [[Logic programming]] |
||
⚫ | |||
* [[Safety-critical systems]] |
* [[Safety-critical systems]] |
||
+ | * [[Computational logic]]<!-- compulog/ --> |
||
⚫ | |||
⚫ | |||
* [[Image:star11t.gif|*]] [http://shemesh.larc.nasa.gov/fm/fm-humor.html Some Formal Methods Humor] |
* [[Image:star11t.gif|*]] [http://shemesh.larc.nasa.gov/fm/fm-humor.html Some Formal Methods Humor] |
||
+ | * [[Image:star11t.gif|*]] [http://critical.eschertech.com/ David Crocker's Formal Verification blog] |
||
* [http://www.thesaurus.com/thesaurus/roget/I/ Words expressing abstract relations] from [http://www.thesaurus.com/ Roget's Thesaurus] — could be useful in describing [http://www.cs.nott.ac.uk/ef-cgi/RogetRequest.cgi?Mode=synonym&Word=formal formal] specifications! |
* [http://www.thesaurus.com/thesaurus/roget/I/ Words expressing abstract relations] from [http://www.thesaurus.com/ Roget's Thesaurus] — could be useful in describing [http://www.cs.nott.ac.uk/ef-cgi/RogetRequest.cgi?Mode=synonym&Word=formal formal] specifications! |
||
* [http://www.anbar.co.uk/coolsite/computing/areas/theory-of-computation.htm Theory of computation] sites and other [http://www.anbar.co.uk/coolsite/computing/computing.htm computing sites] |
* [http://www.anbar.co.uk/coolsite/computing/areas/theory-of-computation.htm Theory of computation] sites and other [http://www.anbar.co.uk/coolsite/computing/computing.htm computing sites] |
||
* [http://www.links2go.com/topic/Formal_Methods Formal Methods] links from [http://www.links2go.com/ Links2Go] |
* [http://www.links2go.com/topic/Formal_Methods Formal Methods] links from [http://www.links2go.com/ Links2Go] |
||
* [http://www.rational.com/uml/ UML] (Unified Modeling Language) — see also: |
* [http://www.rational.com/uml/ UML] (Unified Modeling Language) — see also: |
||
− | ** [http://www.omg.org/uml/ |
+ | ** [http://www.omg.org/uml/ Resource page] from [http://www.omg.org/ OMG] (Object Management Group) |
− | ** [http://www.2uworks.org/ |
+ | ** [http://www.2uworks.org/ 2U Consortium] (Unambiguous UML) |
− | ** [http://www.puml.org/ |
+ | ** [http://www.puml.org/ pUML] (Precise UML group) |
** [http://directory.google.com/Top/Computers/Programming/Methodologies/Modeling_Languages/Unified_Modeling_Language/ Google Directory links] |
** [http://directory.google.com/Top/Computers/Programming/Methodologies/Modeling_Languages/Unified_Modeling_Language/ Google Directory links] |
||
− | * [http://www.wisdom.weizmann.ac.il/~harel/books/stm.html |
+ | * [http://www.wisdom.weizmann.ac.il/~harel/books/stm.html Statecharts] by [http://www.wisdom.weizmann.ac.il/~harel/ David Harel] |
* [http://www.synalp.org/ Synchronous Applications, Languages and Programs] |
* [http://www.synalp.org/ Synchronous Applications, Languages and Programs] |
||
* [http://www.tptp.org/ TPTP] Thousands of Problems for Theorem Provers |
* [http://www.tptp.org/ TPTP] Thousands of Problems for Theorem Provers |
||
⚫ | |||
⚫ | |||
⚫ | |||
Cited in W.W. Gibbs, [http://cispom.boisestate.edu/cis310emaxson/softcris.htm Software's Chronic Crisis], [http://www.sciam.com/ ''Scientific American''], '''271'''(3):86-95, September 1994. |
Cited in W.W. Gibbs, [http://cispom.boisestate.edu/cis310emaxson/softcris.htm Software's Chronic Crisis], [http://www.sciam.com/ ''Scientific American''], '''271'''(3):86-95, September 1994. |
||
Line 231: | Line 242: | ||
---- |
---- |
||
− | Last updated by [[Jonathan Bowen]], |
+ | Last updated by [[Jonathan Bowen]], 11 March 2021. <br /> |
Further information for possible inclusion is welcome. |
Further information for possible inclusion is welcome. |
||
[[Category:Content]] |
[[Category:Content]] |
Latest revision as of 23:10, 11 March 2021
Formal methods are mathematical techniques for developing computer-based software and hardware systems.
Please update this page or add a new page if you know of relevant online information not included here or would like to maintain information on a particular topic. Use the comp.specification.misc newsgroup, for general formal methods queries. Please link to http://formalmethods.wikia.com if you create a permanent hyperlink to this website. In case of problems, please contact Jonathan Bowen.
Introduction
This document contains some pointers to information on Formal Methods↑, useful for mathematically describing and reasoning about computer-based systems, available around the world on the World Wide Web (WWW). Formal methods are a fault avoidance technique that help in the reduction of errors introduced into a system, particularly at the earlier stages of design. They complement fault removal techniques like testing. Links for accessing online information in the following categories are available:
- Announcement
- Selected resources
- Introductory articles
- Individual notations, methods and tools
- Publications (journals, papers, books, etc.)
- Electronic repositories
- Education resources
- Meetings
- Projects
- Companies
- Organizations
- Who's who
- Selected photographs
- Newsgroups and mailing lists
- Safety-critical systems
- Related topics
indicates new entries.
indicates a (subjectively!) recommended link for especially good online information.
Selected resources
This space will be used to indicate selected new entries and developments in these formal methods pages.
- Formal Methods authors on Google Scholar↑. (30 November 2011)
- Wikified and moved to formalmethods.wikia.com. (10 March 2009)
- Formal methods entries in the Wikipedia encyclopedia (30 October 2005)
- The preferred and stable URL for the Virtual Library formal methods pages is now http://vl.fmnet.info. (30 November 2004)
- Checked and updated main links to formal methods. (22 April 2001)
- Moved to the Centre for Applied Formal Methods, [http://www.lsbu.ac.uk/ London South Bank University↑. (13 January 2001)
- New education resources section by Kathi Fisler added. (23 February 1999)
- Search for newsgroup articles on formal methods in Google Groups. (19 December 1997)
- Some Formal Methods Humour. (25 September 1997)
- FM'99: The World Congress on Formal Methods, 20-24 September 1999. (24 July 1997)
- Photographs from the 1st B Conference, Nantes, France, 25–27 November 1996. (6 December 1996)
- Strategic Directions in Computing Research Formal Methods Working Group, ACM, USA. (16 September 1996)
- B-Core (UK) Ltd are now on-line. (25 June 1996)
- EVES and Z/EVES are now available for on-line distribution. (25 June 1996)
- The Steam Boiler Control Specification Problem by J.-R. Abrial, E. Börger and H. Langmaack. A comparative case study for different formal techniques. Published as LNCS 1165. (2 August 1995)
- Comp.specification.misc newsgroup. (12 July 1995)
- Petri Nets graphical notation. (11 April 1995)
- Tools demonstration information for WIFT95 workshop. (6 April 1995)
- A new LOTOS page. (16 February 1995)
- Information on RAISE language and tools. (19 January 1995, updated 17 August 1999)
- A new section on the B-Method has been added. (6 January 1995)
Individual notations, methods and tools
- Abstract State Machines (ASM). Formerly known as Evolving Algebras.
- ACL2 (A Computational Logic for Applicative Common Lisp) theorem prover, a successor to the Nqthm Boyer-Moore theorem prover.
- ACSR (Algebra of Communicating Shared Resources) and Graphical Communicating Shared Resources (GCSR), a formal language for the specification, refinement, and analysis of real-time systems. See the tools VERSA (Verification Execution and Rewrite System for ACSR) and PARAGON for visual specification and verification of real-time systems.
- Action Semantics, a framework for specifying formal semantics of programming languages.
- Action systems for reasoning about distributed systems.
- aiT WCET Analyzer, an abstract interpretation based static analyzer that computes safe upper bounds for the worst-case execution time of tasks.
- Alloy Analyzer, an object modelling notation that is compatible with development approaches such as UML, Catalysis, Fusion, OMT and Syntropy, strongly influenced by the Z specification language. See Alloy discussion group.
- Algebraic Design Language, a higher-order software specification language.
- Argos, an imperative synchronous language with verification support.
- Assertion Definition Language (ADL), a specification based testing toolset.
- Astrée, an abstract interpretation based static analyzer that proves the absence of runtime errors in C programs.
- Autofocus for specifying distributed systems. First prize winner in the tool competition at FM'99.
- BDDs (Binary Decision Diagrams) for finite-state verification problems.
- B-Method, including the B-Tool and B-Toolkit.
- Boyer-Moore theorem prover (a forerunner of Nqthm and ACL2). Available via ICOT Free Software for use under Unix at ICOT (Japan).
- CADP: a widespread toolbox for the Construction and Analysis of Distributed Processes, developed at INRIA Grenoble
- CASL: Common Algebraic Specification Language, for algebraic specification and development, from CoFI, the Common Framework Initiative.
- CafeOBJ, an algebraic specification and programming language. A successor of OBJ.
- CCS (Calculus of Communicating Systems). A process algebra for concurrent systems.
- Circal (CIRcuit CALculus) System supporting a process algebra which may be used to rigorously describe, verify and simulate concurrent systems. See software.
- CLaReT: The Computer Language Reasoning Tool.
- COLD (Common Object-oriented Language for Design), a wide-spectrum specification language.
- CommUnity, based on category theory. See also CommUnity Workbench.
- Concurrency Factory, a "next generation" Concurrency Workbench toolkit.
- Coq proof assistant: checks proofs about assertions, helps to find formal proofs and extracts certified programs from constructive proofs.
- CSP (Communicating Sequential Processes) including the FDR2 (Failures-Divergence Refinement) tool.
- CWB Concurrency Factory and CWB-NC (The Concurrency Workbench of North Carolina), which includes a LOTOS interface, diagnostic information, etc. Note: The CWB and CWB-NC have a common ancestor, but are each under separate development.
- dL -- differential dynamic logic for hybrid systems verification.
- DisCo specification method for reactive systems including an animation tool, Finland.
- Duration Calculus (DC), an interval logic for real-time systems.
- ESC/Java2 Extended Static Checker for Java tool, using program verification technology. See also JML.
- Escher C Verifier, a tool for formal verification of embedded software written in MISRA-C.
- Estelle Formal Description Technique (IS 9074). See also EDT (Estelle Development Toolset).
- Esterel language and tools for synchronous reactive systems.
- EVES tool, based on ZF set theory, from ORA, Canada. See also Z/EVES which provides a Z notation front-end to EVES.
- Extended ML framework for the specification and formal development of modular Standard ML programs.
- FermaT program transformation system. See also here.
- FormalCheck model checker tool for verifying the functionality of digital hardware designs in Verilog or VHDL, based on the COSPAN model checker.
- HOL mechanical theorem proving system, based on Higher Order Logic.
- HyTech (The HYbrid TECHnology Tool), an automatic tool for the analysis of embedded systems which computes the condition under which a linear hybrid system satisfies a temporal-logic requirement.
- IMPS, an Interactive Mathematical Proof System intended to provide mechanical support for traditional mathematical techniques and styles of practice.
- Interval Temporal Logic (ITL). See also and Temporal and Logic publications.
- Isabelle, a generic theorem prover, supporting higher-order logic, ZF set theory, etc.
- Jape (Just Another Proof Editor). A framework for building interactive proof editors.
- JML (Java Modeling Language), a behavioral interface specification language for Java. See also ESC/Java2.
- KeY An automatic and interactive, verification and test generation tool for Java Card.
- KeYmaera A Hybrid Theorem Prover for Hybrid Systems.
- KIV (Karlsruhe Interactive Verifier). A tool for the development of correct software using stepwise refinement.
- Kronos, a verification tool for safety and liveness properties of real-time systems. Uses timed automata, TCTL (an extension of temporal logic) and model-checking.
- Larch family of languages and tools supporting a two-tiered definitional style of specification. See especially LP, the Larch Prover.
- LeanTAP, a tableau-based deduction theorem prover for classical first-order logic.
- LEGO proof assistant.
- Leo-II resolution-based automated theorem prover for Higher-Order Logic
- LOTOS (Language of Temporal Ordering Specifications).
- LPV Linear Programming based software Validation technology, including proofs and testing.
- Lustre synchronous declarative language for programming reactive systems, including verification.
- MALPAS static analysis tool-set.
- Maintainer's Assistant, a tool for reverse engineering and re-engineering code using formal methods.
- MathSpad structure editor, especially for mathematical calculations.
- Maude system for equational and rewriting logic specification and programming. Influenced by OBJ3.
- Meije tools for the verification of concurrent programs. Includes ATG, a graphical editor/visualizer.
- μCRL (micro CRL), process algebraic language for communicating processes with data.
- mCRL2 a toolset for a process algebraic language and a modal logic with data and time. Successor of μCRL.
- Mizar System, a long-term effort aimed at developing software to support a working mathematician in preparing papers. See also here.
- Model checking at CMU, a method for formally verifying finite-state concurrent systems. Available packages include:
- BDD library with extensions for sequential verification.
- CV, a VHDL model checker.
- CSML and MCB, a language for compositional description of finite state machines and a (non-symbolic) model checker for CTL.
- SMV (Symbolic Model Verifier) model checker for finite-state systems, using the specification language CTL (Computation Tree Logic), a propositional branching-time temporal logic. See also Word-level SMV for verifying arithmetic circuits efficiently. See also NuSMV, a new symbolic model checker.
- Murphi description language and verifier tool for finite-state verification of concurrent systems.
- Nqthm 1992, the latest Boyer-Moore theorem prover. Also accessible via FTP. Includes the Pc-Nqthm interactive Proof-checker.
- Nuprl tool based on intuitionistic type theory.
- OBJ family — OBJ3, 2OBJ, CafeOBJ, etc. Term rewriting and algebraic specification.
- OCL (Object Constraint Language), part of UML.
- Otter, an automated deduction system.
- PEPA, a stochastic process algebra used for modelling systems composed of concurrently active components that co-operate and share work.
- Perfect Developer tool from Escher Techologies Limited.
- Petri Nets, a formal graphical notation for modelling systems with concurrency. See also here.
- Pi-calculus: calculi for mobile processes. See also the Mobility Workbench and a searchable bibliography.
- Pobl. A development method for concurrent object-based programs.
- ProofPower is a commercial tool, developed by ICL, supporting development and checking of specifications and formal proofs in Higher Order Logic and/or Z. Support for Z uses a deep(ish) embedding of Z into HOL, but includes syntax and type checking customized for Z.
- Prover Technology, commercial proof engines.
- PVS (Prototype Verification System) language and tool based on classical typed higher-order logic.
- RAISE (Rigorous Approach to Industrial Software Engineering). Includes RSL (RAISE Specification Language).
- Rapide language and toolset, for building large-scale distributed multi-language systems.
- Refinement Calculus, a formalisation of the stepwise refinement method of program construction.
- RISC ProgramExplorer, a computer-supported program reasoning environment for educational purposes.
- SCR (Software Cost Reduction), a tabular notation for specifying requirements and tools for creating and analyzing requirements specifications.
- SDL (Specification and Description Language) from the SDL Forum Society. See also previous site here.
- Signal/Polychrony language and toolset for synchronous systems. See also the related Esterel and Lustre.
- SPARK (now AltranPraxis) secure subset of Ada, including the SPADE static analysis toolset.
- Spec#, an extension of the C# programming language from Microsoft Research with specification features allowing static analysis using a program verifier.
- Specware automated software development system for stepwise refinement of provably correct code. See also technology transfer information and publication from the Kestrel Institute.
- SPIN is an automated verification tool (model checker), using PROMELA (PROcess MEta LAnguage), a language loosely based on CSP, for finite state systems, such as protocols or validation models of distributed systems, developed at Bell Laboratories. See also p2b, a translation utility.
- StackAnalyzer, an abstract interpretation based static analyzer for computing the worst-case stack usage of tasks.
- StateSim simulator for Statecharts models. Draw your models in Open Office Draw and the run your simulations from StateSim.
- Statestep finite state machine modelling with comprehensive elicitation of unusual scenarios (addressing "corner cases" or the feature interaction problem).
- STeP, the Stanford Temporal Prover.
- TAM'97 (Trace Assertion Method). A formal method for abstract specification of module interfaces.
- Temporal-Rover — formal specification and testing tool based on temporal logic.
- TLA (Temporal Logic of Actions), a logic for specifying and reasoning about concurrent and reactive systems.
- TPS and ETPS, the Theorem Proving System and the Educational Theorem Proving System.
- TRIO language and tools for real-time systems, based on temporal logic.
- TTM/RTTL framework for real-time reactive systems.
- UNITY, a programming notation and a logic to reason about parallel and distributed programs.
- UPPAAL verification and validation tools for real-time systems. Model checking and simulation with a graphical interface.
- VCC, Microsoft Research - Verification of Concurrent C; a sound deductive verifier for C.
- VeriSoft, Bell Laboratories, Lucent Technologies. A model checking tool for systematic software testing of concurrent/reactive/real-time systems. Automatically searches for coordination problems (deadlocks, etc.) and assertion violations. Supports C, C++, etc.
- VDM (Vienna Development Method). See also Overture toolset.
- VIS (Verification Interacting with Synthesis), a system for formal verification, synthesis, and simulation of finite state systems, especially logic circuits. Includes a Verilog HDL front-end.
- X-machines, related to finite state machines.
- Z notation for formal specification and extensions eg. TCOZ (Timed Communicating Object Z) .
See also:
- Formal methods entry and category in the Wikipedia free online encyclopedia.
- Formal Methods Europe (FME) HUB.
- Formal Methods Education Resources: Tool Pages.
- Formal Verification Methods and Tools from the VERIMAG research group, France.
- Formal verification Tools list from David Mentre, Association Gulliver.
Newsgroups and mailing lists
- Comp.specification.misc newsgroup including discussion of formal specification and methods, and other related newsgroups (see comp.specification newsgroups and here if you have news access problems):
- Comp.specification.larch — more specific discussion on the Larch, now an archive.
- Comp.specification.z — more specific discussion on the Z and related notations. See monthly FAQ message (Frequently Asked Questions).
- Comp.software-eng — general discussion on software engineering, including formal aspects. See also the comp.software-eng Software Engineering Archives and FAQ message information especially formal specification.
- News.announce.conferences — announcements of conferences including many specifically on formal methods or with a formal methods content; e.g., see separate page on meetings.
- Search for newsgroup articles on formal methods in Google Groups.
The following electronic mailing lists cover general issues concerning formal methods:
- ProCoS mailing list. FMnet, maintained by Jonathan Bowen.
- ProCoS mailing list. Provably Correct Systems, maintained by Jonathan Bowen.
There are a significant number of mailing lists concerning individual formal methods. Please see the relevant pages for the formal methods of interest for details.
See also information on:
- Concurrent systems
- Logic programming
- Safety-critical systems
- Computational logic
- BNF (Backus-Naur Form notation)
- Formal Methods from BRICS
- Some Formal Methods Humor
- David Crocker's Formal Verification blog
- Words expressing abstract relations from Roget's Thesaurus — could be useful in describing formal specifications!
- Theory of computation sites and other computing sites
- Formal Methods links from Links2Go
- UML (Unified Modeling Language) — see also:
- Resource page from OMG (Object Management Group)
- 2U Consortium (Unambiguous UML)
- pUML (Precise UML group)
- Google Directory links
- Statecharts by David Harel
- Synchronous Applications, Languages and Programs
- TPTP Thousands of Problems for Theorem Provers
- Logical frameworks
- Cleanroom Software Engineering
- Automated reasoning systems (see also systems developed in Germany)
Cited in W.W. Gibbs, Software's Chronic Crisis, Scientific American, 271(3):86-95, September 1994.
See also FormalMethods.com. :-)
Last updated by Jonathan Bowen, 11 March 2021.
Further information for possible inclusion is welcome.