Re: Papers on the Ariane-5 crash and Design by Contract

[paul.johnson@gecm.com (Paul Johnson)]

In article <tz8ohcjv7cc.fsf@aimnet.com>, nouser@nohost.nodomain says...

>What was required here was a simple check that a function argument was
>within a certain range.  That check could have been expressed as an
>Ada type declaration and checked by the compiler at compile time, or
>as a runtime assertion/check. 

The whole point of Eiffel is that the assertions are more than just a
run-time check.  In fact the run-time checking is the least important
aspect of Eiffel assertions.  Far more important are the self-documenting
aspects.  This is where Ada misses out: the fatal exception occured
because the limitations were not properly documented.

>The design team apparently decided that
>either approach was too costly in terms of design or speed and instead
>opted for leaving the code unsafe and documenting the conditions under
>which the function could be used safely. 

They did this by commenting the code, rather than writing it into the
documentation.  Furthermore the exception occured (as I understand it)
because the compiler included explicit range checks in the compiled code,
and the programmers had opted not to include manual range checking and
limiting because of CPU limits.  In other words they had a choice between
checking it once or twice (redundantly), and the single check option had
catastrophic consequences.  The important thing is that neither of these
checks were actually very useful at run-time.  The real cause of the 
Arianne 5 failure was the policy that any exception be treated as fatal
while identical software was used on both inertial guidence units.  Hence
any bug that caused an exception would inevitably lead to self-destruction.

In practice, due to the time at which the exception occured it would have
been better to continue processing because the results in question were not
actually being used.  However if they had been in use then its difficult
to see how any kind of run-time checking could have helped: range limiting
only ensures that the wrong results are produced, and this would have been
as fatal as the exception.

[On annotation and documentation]

>And if the programmer culture on a project is such that
>they don't use Ada assertions, why would they use Eiffel
>preconditions?

Because Ada assertions don't form part of the documentation.  Eiffel
assertions do.  So by writing one piece of code you get both benefits.

Furthermore the "Eiffel culture" is very different to the "Ada culture".
In Eiffel the external assertions are seen as a key component of the
software, while in Ada they are just an optional extra.


>   The exception was due to a floating-point error: a conversion from a
>   64-bit integer to a 16-bit unsigned integer, which should only have
>   been applied to a number less than 2^16, was erroneously applied to a
>   greater number, representing the "horizontal bias" of the flight.
>   There was no explicit exception handler to catch the exception, so it
>   followed the usual fate of uncaught exceptions and crashed the entire
>   software, hence the on-board computers, hence the mission.

>I don't understand these statements at all.

Bertrand is accurately paraphrasing the published report, except for one
point: there was a high-level policy in the Arianne programme that any
exception should cause the shutdown of whatever unit of hardware it
occured in.  The assumption seems to have been that the software was
perfect, and so any exception must indicate a hardware flaw.  Therefore
the correct thing to do with an exception is to shut down and let the 
backup unit take over.  Unfortunately the backup in this case was running
exactly the same software and was receiving basically the same data.
Hence they crashed within a fraction of a second of each other.

There was no exception handler: the exception error message was actually
dumped onto the system bus and interpreted by the guidance mechanism as
real data.  This would have probably destroyed the rocket anyway, but
the fact that both inertial sensors went permanently down made it 
inevitable.

Paul.

-- 
Paul Johnson            | GEC-Marconi Ltd is not responsible for my opinions. |
+44 1245 242244         +-----------+-----------------------------------------+
Work: <paul.johnson@gecm.com>       | You are lost in a twisty maze of little
Home: <Paul@treetop.demon.co.uk>    | standards, all different.