Re: Safety-critical development in Ada and Eiffel

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

Wesley Groleau wrote:

:> Consider the aversion of developers to documenting code. It's viewed by them
:> as a necessary burden which doesn't actually make the software work so there's
:> little motivation to do it. ....
:
:I hope this is not generally true, and I don't think it is.  I think
:that 
:there are far too many that think that way, but OTOH even more just let 
:the documentation slide due to real or perceived schedule pressure.  
:Either way it's a Bad Thing.

Agree.


:> little motivation to do it. Executable assertions, OTOH, actually contribute
:> something (runtime checks) to a running program. Therefore, they have some
:> material value in the mind of a developer and their more likely to use them.
:> The by-product is that the code gets documented for free and the developers
:> actually *want* to do it.
:
:And either way, this part is a Good Thing--if it doesn't also slide 
:for the same reasons.

Agree.


:> :And what does that do to the oft-said statement that Eiffel programmers
:> :put in assertions for unlikely events?
:> 
:> That's what all (or at least most) assertions are. They're catering for the
:> unlikely event that the developer has made a logic error. Most of the time
:> we write code with correct logic but occasionally we make mistakes. These
:> mistakes can often be picked up by an assertion.
:
:This is a good idea for most software.  But I would think that if you 
:know enough to write the assertion, you know enough to track down and 
:eliminate whatever would make the assertion fail.  

This is true only in a few isolated cases. However, what we come up against 
more often is an exponential complexity caused by the number of possible 
execution paths to the routine we are dealing with at any one time. While we
can comfortably grapple with the logic of the actual routine at hand and 
a handful of the more isolated execution paths, we usually haven't a hope 
of dealing with all possible execution paths. There are very few people who 
can handle complexity of these dimensions and they probably prefer to use it 
playing chess with Deep Blue or counting cards in casinos than in developing 
software.

So, disappointed, we admit we're not up to the task of dealing with all the 
possibilities in the system as a whole. What we remember, though, is that 
we're more than capable of dealing with just our routine - that's no problem.
Well, if we can't cope with the system as a whole, how about doing it 
incrementally. If we can prove, step-by-step that each part of the system is
doing the right thing, then we've got the problem beaten - a divide-and-conquer
strategy. Let's think about how we might be able to do that..

To do that, we'll suppose we're developing an Air Traffic Control system 
and we have a concept of aircraft which may be transfered from one controller 
to another. The specific part of the overall ATC system we want to consider
is an operation Assume_Control which takes an Aircraft as a parameter.

So, we have

  procedure Assume_Control (Aircraft: Aircraft_Type) is
  begin
    ...
    My_Aircraft.Add (Aircraft);   -- Add to my set of aircraft
  end;

Well, that's simple enough. Not much can go wrong here ..or can it? We see 
a couple of potential problems:

  1) What if I already control the aircraft and, by mistake, the software that
     tranfers control doesn't realise it? It's likely that our software will 
     corrupt some data, for example leaving us with a duplicate aircraft under
     our control!

  2) We delegate work to other objects to get the job done. What if one of 
     them makes a mistake? Then, by implication, there's also a mistake in *our*
     operation!

We need some way to stop these things happening. 

For 1), we could add a comment to the operation header

       -- Assumes aircraft not already controlled

so the transfer software knows to check this first. That's good but still leaves 
us a little uneasy. Even though the requirement is documented, it's still 
possible to miss or ignore it. We could protect ourselves by checking *ourselves*
that the aircraft is not already controlled by us..

  begin
    if not My_Aircraft.Mine (Aircraft) then
      ...
      My_Aircraft.Add (Aircraft);
    end if;
  end;

That would mean *we're* okay, but what about the caller? There is a serious 
problem here in that the caller's code contains an error. They are calling 
an operation they don't need to. This is misleading and may lead to further 
errors in the caller based on the assumed contextual validity of the call.
Also, the erroneous call will cause problems if, for some reason, the 
implementation of our operation changes so it is no longer benign under these 
conditions. 

What we want is a way to signal to the caller that they've made a mistake and 
need to take corrective action. A very effective way of doing that is by 
raising an exception. This sends a very clear message which cannot be ignored.

So, we add a mechanism to the language whereby we can make the checks *and* 
raise an exception if not satisfied..

  procedure Assume_Control (Aircraft: Aircraft_Type) is
  require not My_Aircraft.Mine (Aircraft)
  begin
    ...
    My_Aircraft.Add (Aircraft);
  end;

Now our operation can only be executed under the right circumstances.

What about case 2)? Here, we want to check that the work we delegated was 
done properly and acheived what we set out to do. In this case, we can 
perform some checks and raise and exception against ourselves to force us 
to fix the problem (possibly by delegating)..

  procedure Assume_Control (Aircraft: Aircraft_Type) is
  require not My_Aircraft.Mine (Aircraft)
  begin
    ...
    My_Aircraft.Add (Aircraft);
  ensure My_Aircraft.Mine (Aircraft)
  end;

which is our final solution. What we are now left with is a component of 
software that we know can only be executed under the intended conditions and 
can guarantee producing the required results. We now move on to the next 
component and repeat the process. Step-by-step, piece-by-piece we construct 
our reliable ATC system. We did so *incrementally* through a divide-and-conquer 
strategy and by being demanding in what we expected of callers and demanding 
of ourselves in producing the correct results.

Sorry if this is a bit Mickey Mouse for some, but some may find this helpful.


[the "doing so" following means checking the validity of all calls]

:In safety-critical 
:software, how can you justify not doing so? 

If timing is so desperate that you can't use assertions, you may *have* to 
do perform this sort of analysis manually.


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