When one wishes to plan a spaceflight for a planetary probe, the equations
of motion for the planets, moons, and the probe are written down,
constraints
concerning the capabilities and objectives of the probe are written down,
and
the system is solved, yielding a mission plan that is optimal with respect
to
some objective function. Having generated the mission plan in this way,
there
is no question that the plan satisfies the laws of orbital mechanics. One
does
not generate a mission plan and then verify later that it satisfies the laws
of
orbital mechanics. Similarly one does not design an aircraft according to
principles other than those of aerodynamics, and then later attempt to
verify
that it follows these principles.
In the area of hardware and software development, one can either develop a
system and then attempt to verify its correctness (post facto verification),
or
follow a path similar to the space probe mission plan (correctness by
construction).
Following correctness by construction, one might make specifications for the
correct operation of the system, and then attempt to mathematically derive
the
implementation from the specification. There has been some research along
these lines, including such languages as OBJ, CLEAR, and ML. What these
have in common is that they rely heavily on a rather rich mathematical
setting,
namely category theory. There appears to be some sheaf theory creeping in as
well.
I am currently evaluating this correctness by construction technology to see
if
it is ready for practical application here at Motorola. With this as a
background,
I would like to state my positions on what QED could do for the industry:
1. I hope that the mathematical synthesis of hardware and software
(correctness by construction) will become the method of choice for
industry, over our traditional ad hoc methods, and over post facto
verification.
2. I would like to execute correctness by construction in a rich
mathematical environment. To take an extreme example, if I am
developing
software to control a particle accelerator, I might like to have all
the
mathematics necessary to do theoretical physics at my disposal, and not
start out from set theory, with or without the axiom of choice.
3. I think the verification technology may be appropriate in
establishing
the soundness and/or consistency and/or correctness of the mathematical
environment provided for me to do my correctness by construction.
4. I think that there may always be extremely low level components in
hardware and software that are just too "grundgy" to do in a top down
correctness by construction manner, and may have to be tackled with
post facto verification. I think these woule be extremely small,
isolated
layers of a system.
Many thanks for an interesting debate.
Peter White, Motorola GSTG
----------
From: owner-qed
To: dam
Cc: qed
Subject: Re: Who are the intended customers of QED?
Date: Monday, October 31, 1994 1:20PM
David McAllester wrote:
> The main source of economic support seems to come from applications to
> hardware and software verification. I suspect that the impediments to
> practical verification in engineering are very similar to the
> impediments to practical verification in mathematics.
I suspect the opposite. As I don't have a coherent argument yet,
let me just list some random observations:
(1) In verification one often needs to deal with very large formulas
(say, 300 lines long), but not in mathematics.
(2) BDD's (binary decision diagrams) have revolutionized the
verification of certain kinds of systems, but do not seem to
have any impact on the formalization of "real mathematics".
(3) The mathematics needed in verification is usually very elementary,
eg, elementary graph theory. In fact, it is so elementary that
mathematicians have never found the need to formalize it!
(Eg, when I need some formal graph theory to verify distributed
algorithms, I couldn't find any.)
(4) In mathematics one is interested in the "basic ideas" behind a theory
and usually do not bother to work out all the gory details. But in
verification the "basic ideas" behind a program are usually not in
doubt at all; rather, one is interested in making sure that all the
gory details have been taken care of, because programs are to be
executed by dumb machines that blindly follow instructions.
(5) Many algorithms (eg, many mutual exclusion algorithms) that one feels
need to be verified are "tricky" but not "deep", in the sense that
one does not need any deep mathematics to verify them. On the other
hand, the kind of hand-waving arguments one finds in ordinary math
textbooks are just not rigorous enough to catch all bugs.
- Ching Tsun