Re: Safety-critical development in Ada and Eiffel

[donh@syd.csa.com.au (Don Harrison)]

Ken Garlington wrote:

:Again, someone needs to explain how these high-level assertions would
:have
:benefitted the Ariane 5 IRS.

I have almost zero interest in the Ariane failure because (as Robert Dewar 
correctly pointed out some time ago) it reveals next to nothing about software
engineering except what is blindingly obvious.


:> So, here's a different example. In my key handling object (one of the highest
:> level in the simulation), there's an operation for interpreting the CLEAR key.
:> Simplifying a little, pressing this key should reactivate the menu, clear the
:> key sequence and clear any menu or sub-menu selection. So, there's a compound
:> postcondition thus:
:> 
:>       if SA.ASSERTIONS_ON and then (INPUT_STATE /= MENU or else
:>         NO_OF_KEYS /= 0 or else MENU_OPTION_SELECTED or else
:>         SUBMENU_OPTION_SELECTED) then
:>         raise SA.POSTCONDITION_ERROR;
:> 
:> Note that some of the components are functions. Wrapping them in this way
:> is typical practice in Eiffel and enables you to use them elsewhere (eg. in
:> if-statements in the code proper) and makes contracting scalable.
:
:In Eiffel, I assume this code would be in the "short form." Is the
:user/reviewer
:really expected to read all of this (including looking up the functions
:embedded
:in this code) and understand it?

First, part of the reason it looks complicated is that it is only emulating 
(in Ada83) the real thing. As I've already said, I wouldn't implement assertions
this way if I had the proper tools to work with. If you express it in Eiffel, 
it becomes simpler. 

Second, the compound condition represents a single higher level condition 
which can be declared as a function.

So, expressing it in Eiffel and wrapping the compound condition, we have

  ensure in_menu_state

with function in_menu_state defined as

  in_menu_state: BOOLEAN is
  do
    Result := ...               -- compound condition
  end.

This should be simple enough for any reviewer. The meaning of in_menu_state 
is self explanatory but if they want more detail, they can look at its
implementation.

:Wouldn't it be just as easy to say, in the description of this
:operation, the
:English text preceding it?

..and lose the benefit of being able to execute it?


:... So, unless you propose teaching DBC
:to all engineers in the program (which might not be a bad idea,
:actually),

I agree, it would.


:> With regard to whether an Eiffel software engineer would have
:> picked up the false assumption compared with an Ada SE - possibly, due to the
:> fact that they are conditioned by their use of contracting to *think* of as
:> many assumptions as possible so they can code them as assertions. This sort of
:> conditioning is much less prevalent among Ada developers because most don't
:> use contracting (in this disciplined sense). I *know* this is true because I
:> work with them. Of course, they may be (and probably are) more disciplined
:> in your domain simply because they *have* to be. However, the conditioned
:> cultural difference due to disciplined contracting would be an advantage.
:
:Our engineers are taught the same thing in ADARTS, so I don;t think this
:is
:as big a difference as you think.

I don't know what ADARTS is but it's one thing to be told you have to think
of all assumptions and another to demonstrate you have as evidenced by coded 
assertions.

:I also challenge whether or not you code all of the assertions you can
:envision.
:Look at your example from earlier. There's absolutely no other
:assertions you
:could consider? 

There may be others but so what? The existence of any I may not have thought 
of doesn't negate the effectiveness of those I *have* thought of.

:How about the possibility that calling one of the
:functions
:in the assertion causes NO_OF_KEYS to become non-zero, just for fun?

As I don't write functions with side effects, I'm not sure why I would want to
do that!..


:> For your domain it's a bit of a Catch-22. Contracting would improve the culture
:> but you're unable to use it due to hard timing constraints.
:
:Not at all. We have to distinguish between "contracting" and
:"assertions." You
:can still think in terms of writing strong interfaces, with well
:documented
:user constraints (ADARTS term), but without coding them. For example,
:you may
:write your test cases such that pre-conditions, post-conditions, and
:invariants
:are checked outside the object code. You can also permit more
:comprehensive
:reviews by documenting them via comments. The point is, you don't have
:to use
:DBC/Eiffel to get these benefits... they are also contained in
:ADARTS/Ada, for
:example.

Documented contracts are a good idea and may be appropriate for your domain.
Their weakness is that they can't be enforced, so for *other* domains, I would 
prefer executable assertions.


:> No, it's the conditioning that makes the difference. There are a lot of
:> Ada software engineers who *are* serious about quality (including you, I expect).
:> Using DBC just makes you more effective.
:
:However, the supposed advantage of Eiffel is that this thinking becomes
:code.
:I don't see the advantage for my domain (although I certainly do for
:others).

Agree.

[...]


:> Can you give an example? Not sure how high-level you mean.
:
:Recent examples:
:
:  Ariane 5 - incorrect operational profile (Ariane 4 specified instead
:of 5)
:             See:
:http://www.esrin.esa.it/htdocs/tidc/Press/Press96/ariane5rep.html

There already was one, but it would be better to also have a higher level 
one for initialisation. This would aid testing in that if you fed in the 
wrong profile, you could verify that the IRS will not work. It wouldn't rely
on the more obscure low-level assertion that was actually violated.

In IRS:

  set_operational_profile (profile: OPERATIONAL_PROFILE) is
  require profile_compatible (profile)
  do .. end

BTW, this is intended to suggest what ought to done in engineering such 
software. This presupposes (among other things) that someone has actually sat 
down recognised the dependency of the IRS on the rocket dynamics. It is *not* a 
slap-on "remedy" to the non-existent software engineering that was practised 
in reality.

:  F-18     - divide by zero at Mach 1, due to incorrect control law
:equation in spec.

There already was a predefined assertion for this - "you may not divide 
zero" - which presumably resulted in a numeric_error. This assertion correctly
exposed an incorrect formula(?).

:  YF-22, Gripen - PIO due to incorrect control law equation in spec.
:  (PIO is a complex lag interaction between the operator and the system -

  class SOME_CLASS
    ...
  invariant not PIO (..)
  end

Likewise, this would expose the incorrect formula.


:Aren't there more fundamental problems than just this? You state that
:the assertions can't be executed in a hard real-time thread, so how does
:a "realtime" library help?

For those that aren't.


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