Re: N-version software compared to others

From:         Tom Speer <speer%do.edw@mhs.elan.af.mil>
Organization: 412th Test Wing / TSFF
Date:         10 Jul 96 12:47:15 
References:   1 2 3 4
Followups:    1
Next article
View raw article
  or MIME structure

Peter Hamer wrote:
>
>...
> If the weak-link in N-version programming is the fact that the requirement
> is ambiguous and difficult to understand, surely the same holds true for
> formal methods? The formalization of the requirements might be internally
> water-tight, but its chances a of capturing the intentions of a large and
> complex informal spec are questionable.
>...

It's certainly true that specifying the requirements is the most critical
and difficult part of software engineering.  I have never personally used
formal methods, so I'm only speaking from second hand knowledge here.  But
my impression from talking to some of those who have developed the methods
is that the requirements specification is the area that will require the
biggest culture change when one uses formal methods.

On the STOL/MTD program I wanted to try to express the flight control
software specifications in PROLOG logic statements with the aim of being
able to identify possible states which were undesireable.  This was before I
knew anything about formal methods.  I was unsuccessful in the attempt, and
a big reason was that the requirements came in all different forms, and it
was a major effort to try to combine them into a single form.  And let's
face it, this is essentially what software design and coding is all about.

You really need to start with the method at the outset, and then use your
chosen language to express all the requirements from the top level on down.
The big advantage that formal methods gives you at this stage is that the
specification is comprehensive - it covers not only what the software must
do, but what it must not do.  I suspect that the process of formally
expressing your requirements also helps to uncover "fuzzy thinking" in the
process, and thus may lead to a better specification.

However, I agree completely that formal methods do not substitue for
engineering competence and the knowledge that you need to solve the problem
in the first place.

TS