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