comp.lang.ada
 help / color / mirror / Atom feed
From: Karel Th�nissen <thoenissen@hello.nl>
Subject: Re: Ariane-5: can you clarify? (Re: Please do not start a language war)
Date: 1997/03/19
Date: 1997-03-19T00:00:00+00:00	[thread overview]
Message-ID: <3330541E.61AB@hello.nl> (raw)
In-Reply-To: tz8ohcjv7cc.fsf@aimnet.com


nouser@nohost.nodomain wrote:
> 
> There are multiple ways of reducing the probability of a catastrophic
> software defect like Ariane 5.  Two of them are the following.
> (1) You can test more, enable runtime checks, and implement multiple
> levels of exception handling and recovery.  (2) You can adopt a Design
> by Contract methodology.
> 
> (1) strikes me as more fundamental and powerful than (2).  Design
> by Contract is clearly useful, but secondary if a system isn't built
> on a solid and safe substrate in the first place.  Of course, (1)
> costs more money and may also reduce payloads, but that additional
> expense is paid back in lowered risk.

I disagree: ASSERTIONS COULD HAVE DISQUALIFIED THE SOFTWARE EVEN BEFORE
TESTING,
THE USE OF ASSERTIONS DURING TESTING DEPENDS ON THE QUALITY OF THE TEST
SET
AND ON-FLIGHT THERE IS NO USE WHATSOEVER FOR ASSERTIONS 

The problem is: no amount of runtime checks, tests, contracts or
assertions can gracefully handle on-flight the type of error that
occurred. It is just impossible to convert a 64-bit number with at least
17 significant bits into 16-bit representation. This 16-bit software (as
far as the representation of flight data is concerned) should not have
been taken into space. Truncation or provision of best guesses instead
of exact data would not have stalled the system, but the error in
trajectory calculations would accumulate to such heights that self
destruction becomes inevitable, albeit perhaps a few seconds later than
now.

THERE COULD NOT POSSIBLY HAVE BEEN A ROLE FOR ASSERTIONS ON-FLIGHT

a) Having the assertions unchecked will cause exceptions somewhere later
in the program (with probably the same disasterous effect) or give
erroneous results. Very likely, either case will give raise to the
destruction of the launcher. The only thing we do know for sure then is
that program behaviour becomes hard to predict. As the software was not
performing an essential task (oh irony), the latter may not have given
problems for this launch (by luck rather than science), but from a
software engineering point of view that makes no difference. It was
known that the calculations were, in fact, superfluous, but the software
was believed to be reliable and harmless and that was proven wrong. This
time, it was an exception gone astray in the superfluous subsystem, next
time it is in an essential part.

b) Having the assertions checked on flight does not bring us much
further either, because there is no way to handle the conversion
problem, except by having a similar routine with, say, 32-bit
representation. But if we expect that 32-bit routine to be used, we
would not use the 16-bit software in the first place. And still then,
there is always a risc that even more bits than 32 may be needed. At
this point an assumption about the maximum horizontal bias has to be
made and any assumption about the outside world can prove wrong. It was
assumed that 16 bits were sufficient, and under that assumption the
software was correct. And for the programming team there was no reason
to believe that the 16 bit representation would cause problems, as the
software was developed for Ariane 4. Unfortunately, that assumption was
neither specified as a clear ex-ante or ex-post specification for the
software. This allowed for reuse outside the applicability range of the
software.

!!! THIS SOFTWARE SHOULD NOT HAVE BEEN TAKEN INTO FLIGHT FOR ARIANE 5,
NO MATTER HOW MANY SAFEGUARDS !!!

However, assertions and the like can be very useful on the ground.
Proper tools can signify the assumptions and report them as ex-post
specifications of the software module as a whole. Assumptions are all
those assertions that raise exceptions that are not properly caught and
handled by exception handlers. Then during assembly for Ariane 5, one
would have seen that one of the assumptions regarding the SRI was not
met. Assertions in this respect can be viewed as reporting aid from the
programmer who made an essential design decision somewhere deep down in
the software (it was documented somewhere, so the programmer(s) were
aware of this design decision), up to those who are going to test,
verify or use the software. Any tester or verifier worth his income
would have noticed the invalid assumption (for Ariane 5) that emerged
from the implementation.

Of course, there still is the possibility that these ex-post
specifications would not be used, but that at least supposes an extra
level of incompentency or negligence (by this I do not want to insult
the people on the Ariane project by suggesting that currently there is
incompetence or negligence).

Notice, that hand-crafted documentation or free formatted in-code
comments are too unreliable for this purpose and that normal condition
testings in the software do not necessarily signify assumptions.
Therefore, assertions as a means of documentation add an additional
layer of security that could not easily and reliably be obtained by
other coding practices.

Of course, there are a lot of spots in the entire SRI project where
different decisions at the time may have saved the launcher. But most
decisions seemed perfectly reasonable, both the decisions during the
development of the system and later for its reuse.

Testing might have revealed the software fault, this time, but next time
a fault will get uncaught. Surely, now that we know the bug, it is
simple to think of nice tests that would have relealed the bug
cheaplier. Testing can reveale the presence of bugs not the absence. At
some point one must stop testing, and the team thought it had arived at
that point. Testing was not forgotten, but argued obsolete. Maybe this
is not entirely true:

FLIGHT 501 WAS A TEST FLIGHT, SO THE SOFTWARE WAS TESTED, AND THE
PRESENCE OF BUGS WAS PROVEN, THEREFORE TEST FLIGHT 501 WAS A SUCCESS.

Any piece of software has a applicability scope. Outside this scope the
software becomes indeterminate. Assertions are an important (and
automatic!) aid in the documentation of this applicabilty scope. NEVER
DO WITHOUT THEM.

Groeten, Karel




  parent reply	other threads:[~1997-03-19  0:00 UTC|newest]

Thread overview: 247+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
1997-03-15  0:00 Papers on the Ariane-5 crash and Design by Contract Bertrand Meyer
1997-03-18  0:00 ` Ariane-5: can you clarify? (Re: Please do not start a language war) Jon S Anthony
1997-03-19  0:00 ` Papers on the Ariane-5 crash and Design by Contract Chris Brand
1997-03-23  0:00 ` the one and only real true kibo
     [not found] ` <tz8ohcjv7cc.fsf@aimnet.com>
1997-03-16  0:00   ` Robert Dewar
1997-03-17  0:00     ` Please do not start a language war (was " Jean-Marc Jezequel
1997-03-18  0:00       ` Richard Irvine
     [not found]       ` <tz8913l930b.fsf_-_@aimnet.com>
1997-03-18  0:00         ` Ariane-5: can you clarify? (Re: Please do not start a language war Roedy Green
1997-03-18  0:00         ` Ariane-5: can you clarify? (Re: Please do not start a language war) Gavin Collings
1997-03-18  0:00       ` Please do not start a language war (was Re: Papers on the Ariane-5 crash and Design by Contract Ken Garlington
1997-03-19  0:00         ` Jean-Marc Jezequel
1997-03-19  0:00           ` Richard Kaiser
1997-03-21  0:00           ` Ken Garlington
1997-03-21  0:00             ` Jean-Marc Jezequel
1997-03-25  0:00               ` Ken Garlington
1997-03-26  0:00                 ` Trust but verify " Robert S. White
1997-03-25  0:00                   ` Bertrand Meyer
1997-03-26  0:00                     ` Robb Nebbe
1997-03-27  0:00                     ` Ken Garlington
1997-03-28  0:00                       ` Jeffrey W. Stulin
1997-03-31  0:00                         ` Ken Garlington
1997-03-28  0:00                       ` Karel Th�nissen
1997-03-28  0:00                         ` Ken Garlington
1997-04-07  0:00                           ` Jean-Marc Jezequel
1997-03-29  0:00                     ` the one and only real true kibo
     [not found]         ` <199703190839.JAA02652@stormbringer.irisa.fr>
1997-03-19  0:00           ` Please do not start a language war " Ken Garlington
1997-03-20  0:00             ` Robert S. White
1997-03-20  0:00               ` John L. Ahrens
1997-03-20  0:00               ` Martin Tom Brown
1997-03-21  0:00                 ` Robert S. White
1997-03-21  0:00                 ` Wolfgang Gellerich
1997-03-20  0:00             ` Roger T.
1997-03-21  0:00               ` Ken Garlington
1997-03-21  0:00               ` Jean-Marc Jezequel
1997-03-24  0:00                 ` Ken Garlington
1997-03-17  0:00   ` Paul Johnson
1997-03-17  0:00     ` Enrico Facchin - Sartori E.T.
1997-03-19  0:00       ` Anders Pytte
1997-03-18  0:00     ` Ken Garlington
1997-03-17  0:00   ` John McCabe
     [not found]     ` <tz8n2s1hrdc.fsf@aimnet.com>
1997-03-20  0:00       ` John McCabe
1997-03-20  0:00         ` Jean-Marc Jezequel
1997-03-20  0:00           ` John McCabe
1997-03-21  0:00             ` Niall Cooling
1997-03-21  0:00               ` Gavin Collings
1997-03-27  0:00                 ` Joachim Durchholz
1997-04-03  0:00                   ` Gavin Collings
1997-04-03  0:00                     ` Ken Garlington
1997-04-04  0:00                       ` Derek Clarke
1997-04-04  0:00                     ` Derek Clarke
1997-04-06  0:00                       ` Robert Dewar
1997-04-07  0:00                         ` Ken Garlington
1997-04-09  0:00                           ` Gavin Collings
1997-04-03  0:00                   ` Robert I. Eachus
1997-04-04  0:00                     ` Derek Clarke
1997-04-04  0:00                     ` Chris Beer
1997-04-04  0:00                   ` Ken Garlington
1997-04-04  0:00                     ` Robert Dewar
1997-04-03  0:00                 ` Robin Rosenberg
1997-03-24  0:00             ` Ken Garlington
1997-03-26  0:00           ` Thomas Beale
1997-03-26  0:00             ` Ken Garlington
1997-03-20  0:00       ` John McCabe
1997-03-21  0:00       ` "Paul E. Bennett"
1997-03-22  0:00     ` Nigel Tzeng
1997-03-23  0:00       ` John McCabe
1997-03-17  0:00   ` Robert I. Eachus
1997-03-17  0:00     ` Martin Tom Brown
1997-03-17  0:00   ` Please do not start a language war (was " Jon S Anthony
1997-03-18  0:00     ` Kent Tong
1997-03-20  0:00       ` Ranan Fraer
1997-03-17  0:00   ` Alexander Anderson
1997-03-17  0:00   ` Nick Leaton
1997-03-17  0:00     ` Richard Kaiser
     [not found]     ` <tz8g1xtzx9y.fsf@aimnet.com>
1997-03-18  0:00       ` Anders Pytte
1997-03-18  0:00         ` Jean-Marc Jezequel
1997-03-18  0:00           ` Anders Pytte
1997-03-19  0:00             ` Programming language fanaticism! Louis Bastarache
1997-03-20  0:00               ` Anders Pytte
1997-03-20  0:00             ` Papers on the Ariane-5 crash and Design by Contract Matt Kennel (Remove 'nospam' to reply)
1997-03-24  0:00             ` Joachim Durchholz
1997-03-24  0:00               ` Anders Pytte
1997-03-26  0:00                 ` Robert Dewar
1997-03-27  0:00                   ` the one and only real true kibo
1997-03-29  0:00                   ` the one and only real true kibo
1997-03-29  0:00                     ` Nick S Bensema
1997-03-30  0:00                       ` the one and only real true kibo
1997-03-26  0:00                 ` Matt Kennel (Remove 'nospam' to reply)
1997-03-29  0:00                   ` Anders Pytte
1997-03-29  0:00                     ` Steve Furlong
1997-03-18  0:00           ` Anders Pytte
1997-03-21  0:00           ` Ken Garlington
1997-03-21  0:00             ` Bertrand Meyer
1997-03-21  0:00               ` William Clodius
1997-03-21  0:00                 ` Bertrand Meyer
1997-03-23  0:00                   ` William Clodius
1997-03-23  0:00                   ` the one and only real true kibo
1997-03-22  0:00               ` Fergus Henderson
1997-03-22  0:00                 ` Bertrand Meyer
1997-03-23  0:00                   ` the one and only real true kibo
1997-03-23  0:00                     ` Anders Pytte
1997-03-24  0:00                   ` FUD (Re: Papers on the Ariane-5 crash and Design by Contract) Alexander Anderson
1997-03-24  0:00                   ` Alexander Anderson
1997-03-23  0:00               ` Papers on the Ariane-5 crash and Design by Contract Anders Pytte
     [not found]                 ` <3335BC24.13728473@eiffel.com>
1997-03-23  0:00                   ` Bertrand Meyer
1997-03-24  0:00                     ` Robert Dewar
1997-03-31  0:00                       ` Ken Garlington
1997-04-01  0:00                         ` Bertrand Meyer
1997-03-25  0:00                     ` Ken Garlington
1997-03-24  0:00                 ` Ken Garlington
1997-03-24  0:00                 ` the one and only real true kibo
1997-03-24  0:00               ` Ken Garlington
1997-03-26  0:00                 ` Robert Dewar
1997-03-26  0:00                   ` Ken Garlington
     [not found]                     ` <E7ox17.MKx@syd.csa.com.au>
1997-03-28  0:00                       ` Ken Garlington
1997-03-24  0:00               ` John Hogg
1997-03-18  0:00         ` Laurent Moussault
1997-03-18  0:00     ` Richard Kaiser
1997-03-18  0:00       ` Nick Leaton
1997-03-18  0:00         ` "Paul E. Bennett"
1997-03-19  0:00           ` Nick Leaton
1997-03-24  0:00           ` Joachim Durchholz
1997-03-25  0:00             ` Robert Dewar
1997-03-31  0:00               ` Joachim Durchholz
1997-04-02  0:00                 ` Robert Dewar
1997-04-03  0:00                   ` Martin Tom Brown
1997-04-04  0:00                   ` Derek Clarke
1997-04-04  0:00                   ` Jonathan Egre'
1997-04-06  0:00                     ` Robert Dewar
1997-04-06  0:00                       ` Nick Roberts
1997-03-31  0:00               ` Jan Galkowski
1997-03-31  0:00             ` Alexander Anderson
1997-04-01  0:00             ` Alexander Anderson
1997-04-02  0:00             ` Ken Garlington
1997-03-20  0:00         ` John the Hamster
1997-03-18  0:00     ` Richard Kaiser
1997-03-18  0:00       ` Jean-Marc Jezequel
1997-03-19  0:00         ` Ken Garlington
1997-03-18  0:00       ` Nick Leaton
1997-03-19  0:00         ` Richard Kaiser
1997-03-19  0:00           ` Fergus Henderson
1997-03-19  0:00           ` Jean-Marc Jezequel
1997-03-19  0:00             ` Richard Kaiser
1997-03-17  0:00   ` Bertrand Meyer
1997-03-18  0:00     ` John McCabe
1997-03-18  0:00       ` Ray McVay
1997-03-27  0:00         ` Robert Dewar
1997-03-29  0:00           ` the one and only real true kibo
1997-03-30  0:00             ` Nick Roberts
1997-04-06  0:00             ` Doctorb
1997-04-08  0:00         ` Ron Crocker
1997-04-11  0:00           ` Richard Riehle
1997-03-18  0:00   ` Ulrich Windl
1997-03-18  0:00   ` Jon S Anthony
1997-03-18  0:00   ` Robert I. Eachus
1997-03-18  0:00   ` Jon S Anthony
1997-03-18  0:00   ` Jon S Anthony
1997-03-19  0:00     ` Ron Forrester
1997-03-21  0:00       ` Ken Garlington
1997-03-22  0:00         ` Ron Forrester
1997-03-18  0:00   ` Jon S Anthony
1997-03-18  0:00   ` Ken Garlington
1997-03-19  0:00     ` Eric M. Boyd
1997-03-19  0:00       ` Jeffrey W. Stulin
     [not found]       ` <3345cd60.2092398@news.sydney.apana.org.au>
1997-04-03  0:00         ` Ariane-5 crash , Eiffel and Ada Nick Leaton
1997-04-03  0:00         ` Jeffrey W. Stulin
1997-04-08  0:00         ` AdaWorks
1997-03-18  0:00   ` Papers on the Ariane-5 crash and Design by Contract Tarjei Jensen
1997-03-19  0:00   ` Nick Leaton
1997-03-19  0:00   ` Jon S Anthony
1997-03-20  0:00     ` Jean-Marc Jezequel
1997-03-24  0:00       ` Ken Garlington
1997-03-20  0:00     ` Paul Johnson
1997-03-24  0:00       ` Ken Garlington
1997-03-24  0:00         ` Design by Contract in C++ (was Re: Papers on the Ariane-5 crash and Design by Contract) Anders Pytte
1997-03-19  0:00   ` Karel Th�nissen [this message]
1997-03-19  0:00   ` Papers on the Ariane-5 crash and Design by Contract Karel Th�nissen
1997-03-19  0:00   ` Ken Garlington
1997-03-20  0:00     ` Martin Tom Brown
1997-03-21  0:00       ` Frank Manning
1997-03-21  0:00         ` Martin Tom Brown
1997-03-23  0:00           ` Frank Manning
1997-03-25  0:00             ` Ken Garlington
1997-03-20  0:00     ` Richard Kaiser
1997-03-24  0:00       ` Ken Garlington
1997-03-19  0:00   ` Ken Garlington
1997-03-19  0:00   ` Jon S Anthony
1997-03-19  0:00   ` Karel Th�nissen
1997-03-20  0:00   ` Robert I. Eachus
1997-03-20  0:00   ` Ariane-5: can you clarify? (Re: Please do not start a language war) Nick Leaton
1997-03-20  0:00   ` Papers on the Ariane-5 crash and Design by Contract Robert I. Eachus
1997-03-20  0:00   ` Ariane-5: can you clarify? (Re: Please do not start a language war) Nick Leaton
1997-03-20  0:00   ` Karel Th�nissen
1997-03-21  0:00   ` Papers on the Ariane-5 crash and Design by Contract Alexander Anderson
1997-03-23  0:00     ` "Paul E. Bennett"
     [not found]   ` <tz8sp1qiywm.fsf@aimnet.com>
1997-03-21  0:00     ` ae59
1997-03-21  0:00   ` Ulrich Windl
1997-03-21  0:00   ` Please do not start a language war (was " Jon S Anthony
1997-03-22  0:00   ` Bertrand Meyer
1997-03-23  0:00     ` Dale Stanbrough
     [not found]       ` <3335E18E.33590565@eiffel.com>
1997-03-23  0:00         ` FUD (Re: Papers on the Ariane-5 crash and Design by Contract) Bertrand Meyer
1997-03-24  0:00           ` William Grosso
1997-03-24  0:00             ` Brad Appleton
1997-03-24  0:00             ` William Clodius
1997-03-24  0:00             ` Bertrand Meyer
1997-03-24  0:00     ` Papers on the Ariane-5 crash and Design by Contract Robert Dewar
1997-03-24  0:00       ` Manners (was Re: Papers on the Ariane-5 crash and Design by Contract) Bertrand Meyer
1997-03-25  0:00         ` the one and only real true kibo
1997-03-22  0:00   ` Papers on the Ariane-5 crash and Design by Contract Bertrand Meyer
1997-03-22  0:00     ` Anders Pytte
1997-03-23  0:00       ` Steve Furlong
1997-03-24  0:00         ` Anders Pytte
1997-03-24  0:00           ` Simulating Eiffel-style assertions (was: Papers on the Ariane-5 crash and Design by Contract) Wolfgang Reddig
1997-03-24  0:00             ` Anders Pytte
1997-03-25  0:00               ` Wolfgang Reddig
1997-03-25  0:00                 ` Anders Pytte
1997-03-31  0:00                 ` Joachim Durchholz
1997-03-26  0:00             ` Alan Brain
1997-03-26  0:00               ` Wolfgang Reddig
1997-03-29  0:00                 ` How old time languages survive EJon
1997-03-22  0:00   ` Ariane-5: can you clarify? (Re: Please do not start a language war) Stuart Yeates
1997-03-22  0:00   ` Papers on the Ariane-5 crash and Design by Contract Jon S Anthony
1997-03-28  0:00     ` Matt Kennel (Remove 'nospam' to reply)
1997-03-24  0:00   ` Ken Garlington
1997-03-24  0:00   ` Jon S Anthony
1997-03-24  0:00   ` Ariane-5: can you clarify? (Re: Please do not start a language war) Ken Garlington
1997-03-24  0:00   ` Papers on the Ariane-5 crash and Design by Contract Alexander Anderson
1997-03-24  0:00   ` Ken Garlington
1997-03-24  0:00   ` Ariane-5: can you clarify? (Re: Please do not start a language war) Ken Garlington
1997-03-24  0:00   ` William Clodius
1997-03-24  0:00   ` Papers on the Ariane-5 crash and Design by Contract Robb Nebbe
1997-03-24  0:00   ` Ariane-5: can you clarify? (Re: Please do not start a language war) Nick Leaton
1997-03-24  0:00   ` Papers on the Ariane-5 crash and Design by Contract Ken Garlington
1997-03-27  0:00     ` Joachim Durchholz
1997-03-31  0:00       ` Ken Garlington
1997-04-06  0:00         ` Joachim Durchholz
1997-03-25  0:00   ` Robert I. Eachus
1997-03-25  0:00   ` Ariane-5: can you clarify? (Re: Please do not start a language war) Ken Garlington
1997-03-25  0:00   ` Ken Garlington
1997-03-25  0:00   ` David Starr
1997-03-26  0:00   ` Papers on the Ariane-5 crash and Design by Contract Ken Garlington
1997-03-26  0:00   ` Jon S Anthony
1997-03-26  0:00   ` Alexander Anderson
1997-03-27  0:00   ` Trust but verify (was " Robert I. Eachus
1997-03-28  0:00   ` Robert I. Eachus
1997-03-28  0:00   ` Jon S Anthony
1997-03-31  0:00   ` Ken Garlington
replies disabled

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox