Re: Safety-critical development in Ada and Eiffel

[Ken Garlington <kennieg@flash.net>]

Jean-Marc Jezequel wrote:
> 
> In article <33CC0548.4099@flash.net>, Ken Garlington <keg0@flash.net> writes:
> >Don Harrison wrote:
> 
> >> You would use them anywhere that a piece of code makes assumptions. For example,
> >> to help avoid the Ariane fiasco, include contracts in the INS(?) that specify
> >> Ariane 4 dynamics. Then, in testing, you will get an assertion violation when
> >> you apply Ariane 5 dynamics to it.
> >
> >This is why my blood pressure goes up!
> >
> >The _Ada_ implementation did generate an assertion violation the very
> >first time Ariane 5 dynamics were applied to it. Unfortunately, the very first time
> >Ariane 5 dynamics were applied to it was at LANUCH!
> 
> >They were not applied earlier, because the contractor assumed that the
> >Ariane 5 dynamics were the same as the Ariane 4, so why spend the money testing
> >to the same conditions already tested earlier? (They were wrong, of course, but they
> >didn't know that at the time).
> 
> At the risk of repeating myself, and reopening a thread beaten to death,
> the all point of design by contract (DBC) is to
> make this kind of assumptions explicit.

Which would not have happened in the Ariane V case.

> Ariane 5 is just a nice striking example
> of working with assumptions that are true at a point in time (Ariane 4) and no longer
> later on (Ariane 5). I think we agreed on this previously.

Yes. However, the assumption would not have been documented via an
Eiffel assertion,
as I claimed and you/Meyer never refuted (except to exclaim,
"casuistry!").

> 
> To sum up your point, you think that DBC, i.e. expressing hidden assumptions with
> Eiffel-like assertions would not have been practicable in this case.
> Others think it would have...

The distinction, of course, is that I gavce specific reasons why it
would not
have happened. Please post the evidence stating that the assertion would
have been
added (beyond the bizarre "Eiffel programmers are more careful"
argument).


> You seem to be a specialist in flight software. We are not. But specialists might,
> from time to time, learn something from people with a broader perspective
> (this is a general statement, I do not claim in particular that I have a broader
> perspective than you, or anyone else for that matter;-).

Unfortunately, the reverse is never true. Generalists never listen to or
learn from
specialists.

Consider the work of "generalists" that is incorporated into my code
today: Ada (Ichbiah
et. al.), object-based design principles (Gomaa/SPC, which in turn is
based on a lot
of previous work), safety-critical design (Levison and many others),
testing practices
(Beizer, et. al.)... there are many examples.

In your work on Ariane V, what specialists in the flight software field
(from
Arianespace or elsewhere) did you use to review your paper prior to its
publication?

After its publication, how many specialists in this field publicly (or
privately)
supported your position? I certainly was not the only one to object
publicly!

> Basically, our arguments failed to convinced you. 

Unfortunately, you failed to even discuss some of the points I (and
others) made.

> Yours failed to convince us.
> That's life, and I hope readers can make their mind themselves instead of
> relying on the one of us who shouts louder.

Yes, perhaps other criteria would be better. What would you suggest?
Company
revenues?

I would have thought practical experience would be a strong
determinant...

> >The other part of the problem was that the _response_ to the assertion
> >violation was wrong. The designer assumed the assertion would occur due to a hardware
> >failure, not a software requirements failure, and so the handler shut down the
> >"offending" hardware, rather than attempting some other action (e.g. replacing the
> >out-of-range value with a "safe" value). Frankly, I don't know that I would have written the
> >handler differently myself.
> 
> Agreed, that's a different problem altogether.

But an important one, if the assertion is left in the code. If the
assertion is removed
from the code, then other risks emerge.

> 
> >According to Meyer, et. al. Eiffel programmers would have written the
> >handler differently, and also they would have known to do the testing
> >differently (even though the requirements specification said that the tests need not change).
> >However, their explanation as to why this is true is far from convincing (basically,
> >that "Eiffel programmers believe in quality" or some such nonsense). Their "analysis"
> >is also on the Web. I've asked them to post my rebuttal to their paper, but I
> >don't know if they ever did.
> 
> Just for the record, I'm still waiting for your rebuttal paper to put it on my web alongside
> with the Computer article.

I thought I sent you the summary from the previous thread. I apologize.
I will go into
DejaNews and re-send it this weekend.

> 
> PS: Ken's post was brought to my attention by a colleague: I don't have time to check the news
> very often these days, and anyway I won't follow-up on this thread to avoid reopening the interminable
> Ariane thread.

Unfortunately, it's already been re-opened. As I feared, people are
using your paper to
"prove" the worth of DBC/Eiffel in safety-critical systems, although no
one has yet
published a list of such systems that have been written in Eiffel.

> 
> --
> Jean-Marc Jezequel               Tel : +33 299 847 192
> IRISA/CNRS                       Fax : +33 299 847 171
> Campus de Beaulieu               e-mail : jezequel@irisa.fr
> F-35042 RENNES (FRANCE)          http://www.irisa.fr/pampa/PROF/jmj.html