Re: Safety-critical development in Ada and Eiffel

[Ken Garlington <keg0@flash.net>]

Don Harrison wrote:
> 
> More than likely the Ariane bug would
> have been picked up by traditional means (since it's fairly obvious) but in
> the event that it wasn't, it would certainly have been identified if
> the assumption was identified and coded as an assertion.

...and the same traditional means (testing to the actual Ariane V data)
were used to test the system (otherwise the assertion would never have
been exercised). Thus:

1. If the assertion was not identified and coded as an assertion, but
traditional means were used, the problem would have been discovered.

2. If the assertion had been identified and coded as an assertion, but
traditional means were NOT used, the problem would NOT have been
discovered.

So, since traditional methods were required anyway, how did adding the
assertion (either the Ada "Operand_Error" or your Eiffel equivalent)
help for this example?

Meyer et. al. argues that, if the system was written in Eiffel, that
the assertion would have been added despite the lack of foundation for
doing so in the specification, and that reviews of the code would have
found the inconsistency between the code and specification, causing the
designers to ask the specification writers why they thought the Ariane V
profile was the same as the Ariane IV. Thus, even without the testing,
the Eiffel system would have uncovered the fault. My argument is that
no designer of a non-trivial safety-critical software system could be
expected to either (a) have such an all-encompassing knowledge of the
total platform to either write or analyze such a complex and subtle
assertion or (b) be willing to add assertions willy-nilly with no basis
in the specification (extranous code being identified as a potential
safety issue in more than one certification scheme).

(As an amusing aside, the defenders of the Eiffel faith were reduced to
calling my objections "casuistry," or using an inappropriate specific
case to prove a general statement. This argument, of course, is using
a specific case to prove a _specific case_. One could argue that the
Eiffel paper produced by Meyer et. al. was a better definition of
casuistry, however!)

> 
> :Or in your own words:
> :
> :> No use of assertions will stop you misinterpreting requirements.
> 
> True, though irrelevant to the point I wasn't making. :)

Not at all irrelevant, unless you claim that assertion writing
is not coupled to requirements (which is a very dangerous claim!).
If you look at failures in safety-critical aerospace software systems
(and I've done more than one study on this),  they tend to be
requirements-driven (e.g. F-18, YF-22, Gripen, Ariane V). More than
one controlled N-version academic study has shown this as well. (One
of the best was where multiple teams implemented a set of flight
control laws, using a basic safety-critical software development
process along the lines of DO-178. There was only one common
fault among all of them - a period in the requirements had been
misinterpreted as a comma due to the poor quality of the paper
version of the control laws!)

You could argue that assertions make the process of eliminating
design faults easier, thus allowing your finite test time to
focus on requirements issues earlier. However, I've talked to
people who build safety-critical aerospace systems (and also read
Safeware,
et. al.) and those kind of issues are usually resolved fairly
quickly in *any* good safety-critical software development process.
There may be some benefit to assertions in this environment, but
it's pretty small when measured against the potential risks.

Again, for a non-safety-critical system, where there may be a
higher proportion of design faults, then you probably do see a
larger benefit (I know I do) for dynamic assertions. For
safety-critical systems that can fail-safe, vs. those that must
fail-operate, I could also see some benefits (although that
class of systems seems to be shirnking every day). However,
beware casuistry! :)

> 
> Don.
> =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-
> Don Harrison             donh@syd.csa.com.au