Line 188: | Line 188: | ||
==Newsgroups and mailing lists== |
==Newsgroups and mailing lists== |
||
− | * [news:comp.specification.misc ''Comp.specification.misc''] newsgroup including discussion of formal specification and methods, and other [news:comp.specification.* related newsgroups] (see [http://www.liszt.com/news/search.cgi?word=comp.specification |
+ | * [news:comp.specification.misc ''Comp.specification.misc''] newsgroup including discussion of formal specification and methods, and other [news:comp.specification.* 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): |
− | ** [news:comp.specification.larch |
+ | ** [news:comp.specification.larch ''Comp.specification.larch''] — more specific discussion on the [[Larch]]. |
− | ** [news:comp.specification.z |
+ | ** [news: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). |
− | * [news:comp.software-eng '' |
+ | * [news: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]. (See here [http://groups.google.com/groups/comp.software-eng here] if you do not have direct news access.) |
− | * [news:news.announce.conferences |
+ | * [news: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]]. (See here [http://groups.google.com/groups/news.announce.conferences here] if you do not have direct news access.) |
− | * [[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 |
+ | * [[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: |
||
− | * Educational issues relating to formal methods in computer science. Email [mailto:formal-methods-request@cs.uidaho.edu |
+ | * 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 [http://www.jpbowen.com/ 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.your mum suck my bottom last night :) |
==Of related interest== |
==Of related interest== |
Revision as of 09:40, 1 April 2011
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 [news:comp.specification.misc 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.
- 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 Duration Calculus and RAISE pages. (31 July 1999 / 17 August 1999)
- 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)
- [news:comp.specification.misc 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.
- 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.
- Autofocus for specifying distributed systems. First prize winner in the tool competition at FM'99.
- 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.
- 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).
- 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.
- 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.
- 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. See also Tools for TLA project.
- 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 - 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
- [news:comp.specification.misc Comp.specification.misc] newsgroup including discussion of formal specification and methods, and other [news:comp.specification.* related newsgroups] (see comp.specification newsgroups and here if you have news access problems):
- [news:comp.specification.larch Comp.specification.larch] — more specific discussion on the Larch.
- [news:comp.specification.z Comp.specification.z] — more specific discussion on the Z and related notations. See monthly FAQ message (Frequently Asked Questions).
- [news:comp.software-eng 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. (See here here if you do not have direct news access.)
- [news:news.announce.conferences 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. (See here here if you do not have direct news access.)
- Search for newsgroup articles on formal methods in Google Groups.
- Comp.specification.* Frequently Mentioned Resources from People Helping One Another Know Stuff (PHOAKS). A count of and link to URLs mentioned in newsgroup articles. See also comp.software-eng resources.
The following electronic mailing lists cover general issues concerning formal methods:
- Educational issues relating to formal methods in computer science. Email formal-methods-request@cs.uidaho.edu to join/leave the list and formal-methods@cs.uidaho.edu to post to the list.
- 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.your mum suck my bottom last night :)
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, 21 October 2010.
Further information for possible inclusion is welcome.