Examples of Formal Methods Elsewhere

Compiled by Howard Bowman

One of our intentions is to keep an up to date list of non-traditional applications of formal methods that we are aware of. The following list serves this purpose by listing applications according to the following topics:

If you know of an application of FM that you think could be added to this list please notify Howard Bowman.

Science

Mathematics

Physics

Although, Peter Wegner's ideas on the relationship between interaction and physics (see for example this paper) do not use a formal method directly, the spirit of Wegner's work is strongly influenced by concurrency theory.

Chemistry

Biology

Chris Tofts work on analysing ant behaviour with probabilistic process algebra, see the publications on this page.

(non-standard) Computing

Formal Methods in HCI

The use of formal methods in modelling and analysing human computer interfaces (see, for example, this page, this page and this page, which also contain many relevant links) is now a sufficiently accepted area of research that it is now only loosely a "non-standard" application of formal methods. However, we include it here because there are many interesting, exciting and novel applications of formal methods that can broadly be placed under the HCI banner.

There is work on modelling the user with formal methods, see for example, the projects Programmable User Modelling Applications and TACIT,
John Rushby et al's work in the formal methods and dependable systems group at SRI on analysing cockpit interfaces using model checking and theorem proving. See for example this paper, this paper and this paper.

Modelling Business Processes

Hussein Zedan et al, at the Software Technology Research Laboratory at the University of De Montfort are working on modelling business processes using modal action logics and interval temporal logics.

Non-standard LOTOS

A list of non-traditional applications of the LOTOS formal method can be found on this page.

Medical Systesm

There is work on using Z to design radiotherapy machines, see, for example, this page, which is a rather original class of satefy critical system.

Humanities and Social Sciences

Cognitive Science

There has been work on formally describing cognitive models and architectures. This typically arises out of HCI usability analysis work.

Work by David Duce, David Duke, Phil Barnard, Jon May et al on syndetic modelling (see, for example, the publications under the title "Mathematical Models of Cognitive Processing" on this page).
Work by Howard Bowman and Giorgio Faconti on modelling the Interactive Cogntive Subsystems architecture using LOTOS, see this page.
Work by Ann Blandford et al on cognitive modelling using logical and set theoretic notations, see the PUMA project.
Paul Curzon's recent work on HOL based usability analysis (see this page).
There has even been a Z specification of the Soar Architecture -
B. Milnes "A Specification of the Soar Cognitive Architecture in Z" Technical Report CMU-CSS-92-169, Carnegie Mellon University, 1992.

Philosophy

Roger Jones discusses how formal methods can influence philosophy on the following page.. For example, he models the Triple-Dichotomy on this page. In a sense, this completes a circle, since the mathematics underlying formal methods is typically logic and set theory and these had their origin in mathematical philosophy.

Creative Arts and Entertainment

Music

Paul Hudak has worked on music composition using functional languages (which although not formal methods are close enough for this entry to be made) and game theory, see this paper.

Chris Johnson et al's work in the Glasgow Accident Analysis Group on describing and analysing accident reports using formal methods. See, for example, this page, this paper or this paper.
Peter Wright et al's work on using Petri Nets to describe accident scenarios, see for example, this paper and other papers on this page. In particular, Michael Harrison has been involved in a number of related applications of formal methods.
Peter Ladkin et al's work on describing user manuals using the temporal logic of actions. See, for example, the WB-Analysis home page, this paper or this paper.
Harold Thimbleby has also done a great deal of work on formal interpretation of user manuals, e.g. the following papers, 0, 1, 2, 3, 4, 5.
Graziella Tonfoni's work on eliminating fuzziness and mis-interpretation in written communication, see for example this page and this (microsoft word) document.

Last modified December 1999.
Contact Howard Bowman if you have problems or comments.