Re: Need help with PowerPC/Ada and realtime tasking

[JP Thornley <jpt@diphi.demon.co.uk>]

In article: <Ds6M4D.E09@world.std.com>  bobduff@world.std.com (Robert A 
Duff) writes:
> I suppose it depends on your definition of "correct".  The
> proof-of-correctness folks define "correct" to mean "correctly obeys the
> formal specification".  To me, that's a bogus definition.  In plain
> English, a "correct" program is one that does what it's supposed to do,
> regardless of whether the specification is wrong.  If you show me a word
> processor that deletes my file when I told it to italicize a word, to
> me, that's incorrect, even if you can show me a (bogus) formal spec that
> says that the "italicize word" function should delete files. 

I'd be more impressed by this argument if the examples (such as 
this and "safety-critical green") were more realistic.
[But see below]

                                                           If you
> show me a flight-control program that crashes airplanes, that's
> incorrect IMHO, despite the fact that you might show me a formal spec
> saying it did what the formal spec says.
> 

OK, a slightly better example (I assume that you don't mean that the 
requirement has a 'crash plane' operation).

But how does this point of view influence the production of the code 
that implements the requirements (other than by asking the software 
engineer to be aware of possible errors and omissions and looking out 
for them - a point that has already been covered in these discussions).

There seem to be three main software engineering steps to implementing 
safety-critical code.

1. Examine the requirements and satisfy yourself that they are 
acceptable.

2. Implement the requirements as specified (a *correct* implementation).
This process can bring out further anomalies in the requirements.

3. Identify any additional potential failures that have been introduced 
by the implementation and deal with them (either at the software or 
the system level).  For example how do you recognise and deal with 
corruption of data stored in RAM.

If you demand a correct/safe implementation in code of a flight control
system from requirements that are incorrect/unsafe then what steps 
would you take to achieve it?

-- 
------------------------------------------------------------------------
| JP Thornley    EMail jpt@diphi.demon.co.uk                           |
------------------------------------------------------------------------