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?
- 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.
- 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:-
- FMs have had a limited up-take in their original area of target
application (system development applications);
- nonetheless they offer powerful specification and verification
capabilities; and
- 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:-
- 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.
- 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.
- 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.
- formal description of games
(children games, board games, electronic games...)
- user manuals
- formalisation and verification of legal, medical, bureaucracy procedures
and protocols
- formalised MUSIC!
- formal representation of novels (narrative text) / theatre / movie plots
- personal/social behaviour of humans and virtual agents
- natural language issues
- Formal user modelling for Human Computer Interaction. A major element
of this is formally interpreting cognitive architectures and it has
some history.
- Formal modelling of biological systems.
- Formal modelling in physics.
I see the current objectives of the Exotic-FM initiative as,
- to show how a formal technique (specification and/or verification)
helps in "non-standard" application areas; and
- to provide examples of "systems" that could most likely profit
from being formalised (but have not yet been).
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.