Re: Safety-critical development in Ada and Eiffel

[Joachim Durchholz <joachim.durchholz@munich.netsurf.de>]

Ken Garlington 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).

<Sigh> that misunderstanding again. The issue in the Ariane-5 paper by
Meyer and Jezequel isn't that the preconditions per se would have
changed anything. The issue is that the preconditions would have been an
integral part of the routine's signature, and thus not likely to have
been overlooked by the team that ported the Ariane-4 code to Ariane-5.
As it were, the preconditions were buried in some obscure part of the
documentation, and management didn't reread everything when they reused
the code (together with its hardware).

The paper may not be very clear in this respect (I got Meyer's view on
the topic from his book, not from the paper), or people might
misinterpret what it's saying.

> 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).

No. They would have written the handler the same way, and documented the
precondition with the routine where it belongs, not in some obscure spec
sheets that are shelved away.

> However, their
> explanation as to why this is true is far from convincing (basically,
> that "Eiffel
> programmers believe in quality" or some such nonsense).

Well, believing in quality is far from nonsense. And assertions do
certainly promote a certain style of quality-mindedness.
It is similar to declaring types for routine parameters. Early C didn't
have them, current C compilers have them. And besides catching lousy
errors, the need to declare parameter types makes the programmers
*think* about what's the right type for a parameter, instead of just
writing it down. A similar mechanism is at work with assertions and
Eiffel programmers.

> They believe that "software is software." and apply the
> expertise in their
> domain to mine.

Well, their finding may have been badly presented, but I think the
"software is software" approach is valid. Of course there are
differences between various levels of safety requirements, but some
basic themes apply all the same - like static typing, or the need to
choose meaningful names, etc. Meyer believes that assertions should be
considered one of these basic themes, and that assertions might have
prevented the Ariane-5 crash, for the reasons given above. (And I'm very
much with him, though I'm not informed enough about the Ariane-5 crash
to decide wether it is a particularly good example of the issue.)

> I am aware of at least one project developing an embedded missile
> controller,
> that did exactly what you describe (in Ada). Here's what happened:
> 
> 1. Their timings changed, which introduced some subtle differences in
> the
> relationships between tasks and external interrupts. Some of these
> subtle
> differences invalidated their original testing.

Timing on that basis is the one thing that Eiffel isn't built for.
Adding a new class might not change subtle timings, it might totally
alter the microscopic behaviour of the program. For example,
non-polymorphic routine calls that could be statically bound by the
compiler might become polymorphic and required a dynamic dispatch.
Fine-tuning code so that certain routines are guaranteed to take at
least x ms and at most y ms sounds to me like a very difficult and
fragile thing to achieve in Eiffel.

> 3. At least one compiler bug was introduced, which was definitely
> unsettling.

That's a problem of compiler quality. Eiffel doesn't guarantee perfect
compilers, but assertions should make bugs less likely.

> The other prong of this is that, while assertions are keen for
> catching
> design problems, I haven't seen much evidence that they catch
> high-level
> requirements problems (not surprising, since the code was presumably
> written
> to match the requirements). In 13 years of developing safety-critical
> embedded systems, our process tends to handle design problems fairly
> early.
> It's those high-level requirements problems where we need the most
> help.

Eiffel is the only language that I know that can scale up to formalizing
high-level requirements. The technique is easy: write a few abstract
("deferred") classes that aren't much more than a set of routine
signatures and assertions.
One can even implement such a system: Just take the design classes as
ancestors for your implementation classes. Descendants must keep the
assertions, so your code is guaranteed to match the specs (in a way -
assertions aren't statically checked).

> But almost all of our safety-critical threads are hard realtime
> threads!
> That's a HUGE limitation for our systems!

Well, if you don't have confidence in the compiler, there isn't much you
can do to remove assertions (or run-time range checking, which are a
limited form of assertions).
But in this domain there's no difference between Eiffel and Ada - the
problem's the same, and there is no satisfactory solution available.

BTW I'm somewhat curious how these subtle timing differences come to
have practical consequences. I'm not a hard real-time engineer, so I'd
expect it doesn't matter if a routine runs faster than expected. How
come that your experience is obviously different?

> What is the process to certify Eiffel compilers as being acceptably
> mature
> (code generation-wise) for safety-critical systems? Is all testing
> performed
> with assertions on and assertions off in all test cases?

There isn't even a testbed available - probably because nobody earnestly
demanded it yet.

> However, what about the topic of this thread (safety-critical
> systems)?
> It sounds
> like there's a lot of limitations as to using (and inheriting)
> assertions for
> this environment.

I think OO in general is difficult to apply here. You obviously need
tight control on the code generated, to control the timings. A good
Eiffel compiler will do a global analysis of the system and apply
inter-routine optimizations. This makes the type of control you desire
difficult, and I'm not sure wether the better reliability is worth the
price.

> > :Of course, Bertand Meyer's Eiffel website insists that even
> > :misinterpretation of
> > :requirements (Ariane V) will be a problem no longer when Eiffel is
> used!
> >
> > Come on. He's not saying that.
> 
> Read his analysis of Ariane V. He says _exactly_ that, and has
> defended
> saying that in multiple newsgroups. A smart person, but not someone
> who knows my domain particularly well.

The Ariane-5 crash wasn't a requirements misinterpretation. It was
overlooking a part of the requirements.

Regards,
Joachim
-- 
Please don't send unsolicited ads.