Exotic Applications of Formal Methods

Exotic Applications of Formal Methods (Exotic-FM)

Howard Bowman

Exotic-FM seeks to foster the application of Formal Methods (FM) to a spectrum of new (exotic) application areas.

Formal Methods Elsewhere

Along with a number of researchers (see for example, this page) I strongly believe that formal methods technology is much more widely applicable than to just computer system development and the Exotic-FM initiative seeks to pursue this view. The main event in this research activity is the workshop:
Formal Methods Elsewhere
which was held as a satellite workshop of FORTE-PSTV-2000.

The proceedings of this workshop were published as volume 43 of Elsevier's Electronic Notes in Theoretical Computer Science and are available here.

Classic Applications of FM

Formal methods have been investigated over a relatively long period, with early work (e.g. on Petri Nets) dating back to the 1960's. Such formal methods research has been performed in the Computer Science domain and has the broad motivation of devising techniques that can be used in the system development process. In fact, a number of early advocates suggested that there would be a wholesale overhaul of the system development process - replacing informal and ad-hoc methods with formal specification, formal verification and formal analysis.

However, although there are now many examples of successful applications of formal methods and in addition, there are some niche areas where there application is routine, they have not infiltrated the mainstream of system development practice.

One possible explanation for this limited up-take is that FM's cannot be easily integrated into current system development practice (for example, they typically require a major notational change). In addition, they still do not map well to existing implementation paradigms, such as imperative programming languages.

However, as formal methods researchers, we remain confident that the fruits of our labours are of value and indeed the recent successful applications of FM in system development give some justification for this view.

So, what then is it that FMs provide? What are their benefits?

  1. FMs support the description of the behaviour of systems in an abstract (non-prescriptive) manner.

    Of particular relevance is the term abstract - programming languages, for example, clearly allow the behaviour of systems to be described. However, they describe this behaviour in a prescriptive manner, i.e. a program defines a single implementation. In contrast, using devices such as non-determinism, FMs typically support more abstract description, where the specification characterises a set of possible implementations.

  2. Formal descriptions of systems are amenable to formal manipulation and analysis. For example, powerful theorem proving and model checking tools now exist. These can be used to determine what properties system descriptions exibit. Futhermore, this analysis can often be performed in an automatic, or at least, semi-automatic, manner.
Despite the disappointments that surround the currently only limited up-take of formal methods, we should not lose sight of the significance of these two benefits. Indeed we would argue that the capacity to write abstract (non-prescriptive) descriptions of system behaviour and then formally analyse these descriptions to determine their emergent properties is a great success story of formal methods research.

Furthermore, the basic principles of FM techniques are often extremely general. For example, the basic concepts underlying a large part of concurrency theory research (particularly process calculi), is that such systems can be viewed as a collection of concurrently evolving components which interact by performing synchonous rendez-vous. These principles are completely general and are in no way bound to the computer science application domain.

Thus, we can summarise what we have argued so far under the following points:-

  1. FMs have had a limited up-take in their original area of target application (system development applications);

  2. nonetheless they offer powerful specification and verification capabilities; and

  3. their underlying principles are often very general in nature.
An obvious response to these observations is to broaden the net of application of FMs. In particular, it is our firm belief that many different types of system - biological, physics, artistic - can be beneficially described and analysed using FMs. This is exactly what Exotic-FM is striving to do.

Non-standard Applications of FM

There are a number of reasons for thinking that such a broadening of the application of FMs might be successful:-
  1. An advantage of specification and verification in a non system development setting is that the problem of mapping to implementations often does not arise. This is because such application areas typically use formal methods solely for modelling and analysis, without the intention of generating an implementation in the computer science sense.

  2. Abstraction can be important in these exotic application areas since programmed interpretations are often too prescriptive and only a loose description of the system under investigation is possible. This might for example be because a complete (deterministic) understanding of the behaviour of the system under investigation is not available or that certain aspects are so prohibitively complex that they cannot be described deterministically.

  3. Formalization brings the possibility to verify the resulting description. Many different forms of verification are possible - reasoning about the description using theorem proving technology, model checking to automatically determine if a particular property holds or even doing performance analysis to determine the varying behaviour of the system. All such techniques have potential relevance for exotic application areas.
To indicate the spectrum of possible exotic applications, I list some possible topics. These have arisen out of a quick brainstorm between myself and Tommaso Bolognesi and are either topics where we know some formal methods work has been done or where we have some intuition that the area could be amenable to formal interpretation. I see the current objectives of the Exotic-FM initiative as, I am personally particularly interested to pursue the "non-standard" application of concurrency theory techniques. This is because, as mentioned earlier, the basic principles of these techniques are extremely general and systems with the following character arise throughout science (and even more broadly):
reactive, interaction based, concurrent, distributed.

Back to Howard Bowman's home page.

Last modified December 1999.