Yes, people are using these things. Much of the use is in
hardware (which has some properties that make the use of
tools like model checkers easier). But the question is HOW
are they using them. I'm most familiar with TCAS. There
have been claims to have model checked it. But they could
only check the boolean logic parts of it, which were the
simplest and no errors were ever found in that part. The
hardest (and biggest) part is the algorithms to determine
whether an aircraft is a threat. That's where all the problems
were found. Those parts could not be model checked because
they contain complex mathematics, so they simply simulated
them. An executable specification language can do that.
That group also came to me and asked me what they should
model check. I told them that was what they were supposed
to decide. In the end, they found only two errors in the
spec they made (which was from our original spec) which
had been found easily by the human reviewers. They did not
find any of the subtle ones not found by the humans (during
the original V&V) that were not found until operational use.
So, again, yes people are using these tools. The question is
how well they are using them. I remember seeing some supposed
formal specifications during the period when the British MOD
still required them. They were nonsense.
I have been working in the field of formal specification and
formal analysis of systems for a quarter century now. These complaints
about "formal methods" could well have been written back then.
People don't like Z. You need a PhD to understand how to use a
language. You can do things in a language readable with 10 minutes'
and it's just as good as formal notations. Logic is too hard for
Engineers have no time to understand computer science. There is no
motivation for using formality. And so on.
Meanwhile, SPIN has turned from a one-man research project into a tool
thousands, indeed you can't design telecommunications protocols any
someone insisting you model-check them. Cadence has a very successful
on temporal-logic model checking, Lockheed Martin praise the use of
SPARK in their C130K
project, Eurocopter uses SCADE in safety-critical parts of the EC135;
so does Airbus in
the A380, the B method has been used on rail lines in Paris, Siemens
uses a code-generator
and model-comparison techniques for building the world's most complex
rail signalling systems,
one of the world's major auto component suppliers uses Parnas tables
a very visible series of technical embarrassments a few years ago.
Intel uses model checkers and theorem provers in the design of its
suffered a very visible embarrassment with a FP processing unit a few
Microsoft is using static analysers and annotated programming
languages for its new
critical products. And so on.
Who really thinks any of those organisations are going to go back to
the way they did them before? The argument about use of formal methods
has obviously been won. But you probably need to be over 50 to have
That said, the specific argument about the use of Z and VDM and CSP
and so on in software
forward development, specifically in requirements, has not been won.
Who here thinks
UML 2.0 will win it?
To my mind, the real issue is rigor and precision. Ensuring those
qualities takes a lot of effort.
It took a lot of effort in the past, and it will take a lot of effort
in the future. There are, have been,
and always will be people who complain about the extra effort is
takes. It is easy to complain,
for safety is the absence of something. If an accident has never
happened to you, you may not
want to put in that extra effort. Then it happens, as to Intel and
Microsoft (continually!) and the major
auto component supplier above, and then somebody in management sees
the business case for
the extra effort and, lo and behold another formal methods user.
And you probably need to be over 45 to get impatient at seeing the
same old arguments
against formal methods as a quarter century century ago being trotted
out yet again.
Really, how can one ignore that the two major computer companies in
the world have had
to start using them in the last decade? Microsoft employs major formal-
methods people such
as Tony Hoare and Leslie Lamport well past the usual retirement ages.
On the other hand, maybe the same old arguments are being trotted out
because there are eternal truths about
the use of rigorous methods in engineering and these are some of them.
If this were so, then, quantifying over time,
we could conclude:
no formal specification languages will ever be readable, model-
checking will never solve anybody's
real problems, theorem provers for refinement and code checking
will never be usable by engineers, static
analysis is only for academics.
Given that all of these already admit counter examples, I wouldn't
recommend believing any of it.
Peter Bernard Ladkin, Professor for Computer Networks and Distributed
University of Bielefeld, 33594 Bielefeld, Germany
www.rvs.uni-bielefeld.de +49 521 880 73 19
Received on Thu 06 Aug 2009 - 15:50:23 BST