Formal Methods Links, by Mark Utting

Contents: General, Specification animation, Model-based testing, Reasoning tools, Object-Orientation, FM Applications, FM Teaching.

The Formal Methods Wiki contains information about all kinds of formal methods and supporting tools.

The three main model-oriented formal specification notations are Z, B and VDM.

FMEInfRes, the Formal Methods Europe Information Resources project also has a formal methods database of applications, tools, bibliographies and FAQs.

The FACS Seminars give some good high-level overviews of various aspects of formal methods.

Praxis Critical Systems produces the SPARK language (an Ada subset) and the SPARK Examiner toolset. They say: SPARK remains the only widely-used, unambigous programming language that supports formal development methods such as B and Z, while being used in large, real-world projects such as EuroFighter, Lockheed C130J, SHOLIS, and the MULTOS CA. They have a free-of-charge release to academic institutions for teaching and non-commercial research purposes. This 2005 IEEE Spectrum article The Exterminators describes their approach and some industrial applications.

NASA have experience in using formal methods and their web site contains many interesting formal methods links, plus two excellent guidelines books on using formal methods.

The Rodin (Rigorous Open Development Environment for Complex Systems) project is developing an open and extensible tool platform based on Event B. There are about four universities and four companies working on this project.

The Community Z Tools (CZT) project is developing open-source support tools for the ISO Standard Z Specification Language, and some languages that extend Z, such as Object-Z and Circus. (I lead the Java development of this project.)

The FormalWARE project was a two-year university/industry collaborative project to investigate potential applications of formal methods in the development of software-intensive, critical systems. They developed a Z-like specification language called S, with some impressive tool support for checking, animating, and generating test sets.

Quality Systems and Software has a requirements management tool called DOORS, that interfaces to the B-toolkit and tracks the relationship between informal requirements and the B specification.

Logica have developed a Z editor ('Formaliser'). They also have a test case generation tool called Zylva, but this runs only under Windows 3.1.

ZEUS is an extension to the Adobe Systems Framemaker editor that allows Z specifications to be edited and analyzed by Z/EVES.

The RISKS Forum documents risks to the public in computers and related systems, including discussions of many accidents caused by computers.

Edsger W. Dijkstra's EWD notes and unpublished writings are now available online.

rbjones.com has lots of introductory pages on logic, and the Factasia pages contain quite a lot of background information on Z (see the 'cs' link).

Carroll Morgan's book `Programming from Specifications' (second edition) is available online.

Vista is a graphical editor and layout tool for Statecharts, with a translator into Z.

The Another's B Tools system has ANTL lexers and parsers for the B notation, developed by Boulanger Jean-Louis.

Animation of Formal Specifications

(See the Z FAQ on this question)

Model-Based Testing

The STORM site (Software Testing Online Resources at MTSU), is intended to be a "first-stop" on the Web for software testing researchers and practitioners.

ModelJUnit is an open-source Java library (written by me) that supports simple model-based testing. Models are written as Java classes, and several test generation algorithms can be used to generate online or offline tests. ModelJUnit is described in Chapter 5 of our book Model-Based Testing: A Tools Approach by Utting and Legeard.

org.tigris.mbt is an open-source implementation of model-based testing built in Java. It allows you to generate test sequences from a finite-state machine (graph). The test sequences can be created statically, or run dynamically. It takes a graphml file as input, so the modelling must be done in a separate tool, such as yEd from yWorks, which is available as a free download with unrestricted functionality. The tool itself does no actual test execution of the generated test sequences -- this must be done by an external tool such as Quick Test Professional, Functional Tester, Win32::GuiTest or even tools made by you.

The BZ-TT project is developing tools for generating tests from B and Z specifications. This is a collaborative French/New Zealand project, and I lead the New Zealand end. LEIRIOS Technologies is now producing commercial versions of these model-based testing tools.

UniTESK builds commercial tools for generating tests from specifications that are written in specialized extensions of traditional programming languages (C, C++, C# and Java). The UniTESK tools are used by the Linux Verification project.

The commercial T-VEC Test Vector Generation System performs automated model analysis, test vector generation, test coverage analysis, and test driver generation to eliminate many manual and error-prone activities involved in verification and testing.

Here is an example of the KVEST system: a RAISE/RSL specification and the tests and documentation generated from it. See the FM99 page 608 proceedings for more about KVEST. KVEST is being extended to handle OO specifications in 1999.

A. Jefferson Offutt has several testing projects, including specification-based testing and mutation testing tools (Mothra).

The Open Fundamental Software Technology Project in Japan were working on an architecture for automated test generation from formal specifications, but the web site has not been updated since 1995.

Tinman is a tool being developed at the University of Queensland to support the interactive construction of Test Template Framework (TTF) trees from Object-Z specifications.

Other interesting testing links:

Reasoning Tools

Most provers are listed on the Stanford Database of Existing Mechanized Reasoning Systems.

Isabelle is probably the most widely used generic interactive theorem prover around.

PVS is probably the mostly highly automated interactive prover. PVS is a verification system: that is, a specification language integrated with support tools and a theorem prover.

The Ergo interactive proof tool was developed at the Software Verification Research Centre (SVRC) during the 1990s. It is based on Qu-Prolog. A recent release is available free, but newer versions are in the pipeline. I have a particular interest in this project, because I worked at the SVRC for five years and managed the Ergo project for most of that time.

The Z/EVES system supports typechecking and theorem proving in the Z specification language, with probably the highest degree of automation currently available for Z. Unfortunately, ORA stopped distributing Z/EVES since 2005.

haRVey, from the CASSIS project in France, works in (a fragment of) first-order logic with equality. It automatically decides the validity of arbitrary boolean combination of ground literals modulo an equational theory (which is assumed to be axiomatized by a finite set of equational clauses). Examples of such theories are the theory of arrays, of lists, and their combination. The system is based on a simple combination of BDDs (to compactly represent the boolean structure of ground formulae) and of superposition theorem proving (to effectively reason in the equational theories). If a formula is not valid, then a sub-formula is returned from which a counter-example can be built.

ACL2 is the latest in the Boyer-Moore line of automatic theorem provers (starting from NQTHM). The system is coded in its own logic, which is an extension of a subset of applicative Common Lisp. This means that you can execute the theorems that you've proved at native Common Lisp speed!

Joseph Goguen's OBJ Family page describes the OBJ family of broad spectrum algebraic programming and specification languages (OBJ3, CafeObj, BOBJ etc.). Execution corresponds to equational theorem proving. OOZE is an object-oriented environment for Z, built on top of the FOOPS system, which in turn is built in top of the OBJ system.

The ILF System contains a Mathematical Library that stores definitions, theorems and proofs from various sources. As a first step it contains a number of articles from the Mizar Mathematical Library.

The QED project is more ambitious, aiming to build a single, distributed, computerized repository that rigorously represents all important, established mathematical knowledge. (Also has a useful list of theorem provers).

The Saturate system is an experimental theorem prover for first-order logic, primarily based on saturation. Saturate uses techniques of ordered chaining for arbitrary transitive relations, including orderings, equivalence relations and congruences, and combines CNF transformation with saturation. It also has inbuilt support for AC operators.

The Maude system, its documentation, a collection of examples, and a list of related papers are available (free of charge) here.

MOCHA is a growing interactive software environment for system specification and verification. The main objective of MOCHA is to exploit, rather than destroy, design structure in automatic verification. Currently, MOCHA offers the following capabilities:

SPIN is a model-checker for LTL (Linear time logic).

Diakon is a tool for dynamically detecting invariants about a program's data structures -- the sort that might be written in an assert statement or a formal specification. Examples include a>0, c=2*d+3, a particular list or array is sorted, the child slots of treenode objects point to objects whose parent slots point back at the original treenode, and the like. Such program properties are useful for a wide variety of software construction, understanding, reuse, and modification tasks, but they are usually absent from code. Static techniques for determining invariants break down in the presence of real-world constructs such as pointers, so the Daikon system takes a dynamic approach -- it examines the values computed during the target program's execution, looking for patterns and relationships among those values.

Object-Orientation (Specification, Refinement, Tools etc.)

Modern Jass (pronounced 'Modern Jazz') uses Java annotations to express preconditions and postconditions and class invariants. These are syntax/type checked at compile time and their truth is checked via runtime checking. A nice alternative to JML.

KeY (Integrated Deductive Software Design) integrates formal software specification and verification into the industrial software engineering processes (such as the Together ControlCentre CASE tool).

The Perfect Developer Tool from Escher Technologies is an object-oriented software development system that goes from specifications to code, with the option of doing proofs for each refinement stage.

JML is Java extended with assertion annotations, in a refinement calculus style. There are several tools available or under development for it, including typecheckers, runtime assertion checkers and an extended static checker (ESC/Java 2) that checks for possible errors like out-of-bound array indexes, calling a method with a false precondition, etc.

The earlier Compaq ESC/Java (Extended Static Checking for Java) project uses formal methods ideas and automatic theorem proving to check assertions and verify runtime checks (array bounds checking, NULL pointer dereferences etc.) at compile time. Their system for doing extended static checking uses program verification technology, but feels to a programmer like a type checker. They also have an interesting concept of virginity in OO systems, which is related to the 'rep' objects of James Noble and John Potter's mode system for flexible alias protection (and perhaps my 'local stores').

See the bottom of the iContract FAQ for a list of other Java Design by Contract notations.

RoZ is a french tool for the production of formal Z specifications from annotated UML diagrams (integrated with Rationale Rose). A brief report on this is in FACS vol 12 number 4, pp.228-230.

ZML: Z family on the web with their UML photos. This is an XML/XSL web browsing environment tool (ZML) that uses Internet Explorer 5 to display Z, Object-Z and TCOZ specifications, with hyperlinks, schema calculus expansion, Object-Z inheritance expansion and transformation/projections to UML diagrams.

On semantics of OO languages, check out Luca Cardelli's 'Theory of Objects' which lists work related to their book.

Applications of Formal Methods

The FME database lists many projects that have used formal methods.

The University of TessSide's B-resource centre has a list of projects that have been done with B (a formal code development tool similar to the refinement calculus).

The Precise UML group (pUML) is using formal techniques, such as Z specifications, to investigate the semantic foundations of UML.

Some other UML related tools with OCL support (as at Sept2003) include:

Teaching of Formal Methods

Teaching equational logic, by David Gries.

An On-Line Repository of Formal Methods Educational Materials. Covers areas such as: computer-aided verification; theorem proving; programming languages; logic; software engineering; security. The site contains pointers to:

The ITiCSE Working Group on Teaching and Learning Formal Methods with Software is producing (by Dec 2000) a report on the support that is available in the area of formal methods education, and to provide guidelines for educators who are coming to teaching formal methods for the first time. Including: how to design a formal methods course; how to manage the teaching, learning and assessment of formal methods; how (and why) to use software.


marku@cs.waikato.ac.nz
Last modified: Thu Jun 4 11:04:08 NZST 2009