RE: Interesting article ZDNet re informal software development quality

["David Crocker" <dcrocker () eschertech com>]

Crispin Cowan wrote:

> >
Software engineering has found a collection of methods (formal methods,
formal specifications, ISO 9000, Common Criteria, etc.) that appear to
produce better software artifacts than just slamming together some crap.
Unfortunately, these methods are *not* satisfactory: not only are they
outrageously expensive, they also fail the reliability test. While they
*tend* to produce software that is better than random methods, they
absolutely do *not* give you the reliable artifact production that
bridge building and boiler engineering methods do.
<<

That may well be true of some methods, but not formal methods.

While formal methods have been "outrageously expensive" in the past, that is no
longer the case. The company I work for specialises in affordable formal methods
(although we prefer to use the term "verified software development"). The reason
for the expense in the past was that a great deal of human effort was involved
in constructing the proofs. These days, we use automated reasoning technology to
construct about 99% of the proofs entirely automatically. Also, many
specifications can be refined to code without user intervention.

As for "they fail the reliability test": all the evidence I have seen shows that
when formal methods are applied to the whole development process (not just the
specification phase) and all the verification conditions are proved, the result
is software that is highly reliable. Of course, if formal methods are used
purely at the specification level, or without proof, then you don't have the
same reliability guarantee.

Even with formal methods, it is still possible to misunderstand the customer
requirements. Formal methods do make it easier to detect incomplete and
inconsistent requirements, but even the customer frequently does not know what
his/her requirements are. It is at the requirements level that the quality
aspects of the process are vital even when formal methods are used.

As for Extreme Programming, one of its great advantages over waterfall is that
it is far more responsive to changes in the requirements. One of our customers
has suggested "Extreme Specification" as a way using the ideas behind XP with
formal methods. Whereas with XP you take one requirement, write the test for it,
implement it and then test it, with XS you take one requirement, specify it
behaviourally (which is equivalent to writing all possible tests for it), refine
it to code and then prove that the code precisely meets the specification (i.e.
prove that it passes all possible tests).

As to the original topic (commercial vs. open source development approaches), I
suspect that open-source development produces worse code than the best
commercial processes, but better code than many (perhaps most) commercial
organisations because of the greater amount of peer review.

David Crocker
Escher Technologies Ltd.
www.eschertech.com
Tel. +44(0)1252 336565  Fax +44(0)1252 320954