Re: Safety-critical development in Ada and Eiffel

[Ken Garlington <keg0@flash.net>]

Don Harrison wrote:
> 
> Ken Garlington wrote:
> 
> :Don Harrison wrote:
> :>
> :> If even this small overhead is unacceptable, you can force static binding
> :> where necessary by freezing routines.
> :> Although you forgo the flexibility of
> :> polymorphism, you can still take advantage of inheritance by virtue of Eiffel
> :> synonyms - these allow you to declare a routine under different names.
> :
> :But I can do this in Ada, as well, so I don't see the benefit.
> 
> I'm not saying there is any extra benefit - merely that you don't have to
> wear the overhead of dynamic binding if you're desperate to maximise efficiency.
> Tucker mentioned that overhead. I'm saying it isn't an issue.

But you also said that it was required to use that part of Eiffel
inheritance not
available in Ada. In this statement, you seem to be saying that if I
want an
efficient safety-critical system (which I always do), I have to give us
some of
that extra inheritance. Do I need the full Eiffel inheritance model, or
don't I?

> 
> BTW, how do call a procedure under different names in Ada?

Via the "rename" statement.

> 
> : :Does this "pre-allocated memory pool" mean that you will know exactly
> :> :what address
> :> :each object's data will reside at, or merely that you dynamically
> :> :allocate memory
> :> :at initialization and do not dynamically allocate after initialization
> :> :is complete?
> :>
> :> The latter. You don't actually need to know *where* objects are allocated,
> :> merely that there is sufficient memory to allocate them.
> :
> :Actually, in my systems, I do need to know where they are allocated, so
> :that
> :I can examine them from the hideously crude display in the cockpit
> :during
> :troubleshooting.
> 
> That *is* hideously crude (and brings back some bad memories). Depending on how
> crude you mean, maybe a primitive tool could give you a map of where objects get
> put in memory. If you mean incredibly crude, use non-reference (expanded in
> Eiffel) types and use a linker-generated memory map.

Both approaches require that the memory address be known before
execution time,
however, so I still care where objects are located. I also care for
other reasons,
such as memory-mapped I/O, of course.

> 
> :> Maybe general assertions are more common than you imagine. However, I agree
> :> that range constraints are roughly covered by Ada subtypes. I use them liberally
> :> for just that purpose.
> :
> :Maybe, but again, I would like to see how these complex assertions are
> :used.
> 
> 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).

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.

This is all clearly documented in the final report, available on the
Web.

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.

This is why I dislike people with no background in safety-critical
flight systems discussing
such issues. They believe that "software is software." and apply the
expertise in their
domain to mine. They usually do about as good a job as when I try to
discuss compiler
design :)

> 
> :Again, the code I've seen to date doesn't seem to use them that much.
> 
> If you're looking in Ada code, you're looking in the wrong place because few
> Ada developers recognise there are additional benefits from using them in
> addition to static typing and the predefined contracts already in Ada
> (the conditions under which predefined exceptions - eg. Constraint_Error -
> are raised).

No - I'm looking at Eiffel code. (Why would I look at Ada code to
determine how
Eiffel is used?)

> Static typing gives you static contract checking. Assertions (predefined and
> user-defined give you dynamic contract checking *during development*. What
> most Ada software engineers miss out on is the user-defined variety which
> bring a non-trivial benefit to reliability and reuse.

Not this Ada engineer! I have dynamic assertions all over the place in
my
tools!

My problem, again, is in the fundamental nature of dynamic assertions
for safety-critical
embedded systems, which have some unique risks, whether you (a) leave
them in after
development, or (b) take them out after developmental testing, but
before usage.

> 
> :> Correct me I misunderstand you.. Are you wondering whether contracting
> :> helps you to identify more bugs? I can offer my own experience which has
> :> firmly convinced me of this.
> :
> :Contracting definitely identifies more bugs. However, my concern with
> :Eiffel
> :assertions (and Ada assertions, for that matter) is that, once raised,
> :it's
> :not always clear what to do about them.
> 
> They are only turned on during development, so what you do is fix the underlying
> problem which is usually not difficult to find if you've used them systematically.
> Even if you haven't (I was the only one of a team of 5 using them in our recent
> development cycle), they still tell you more than you would otherwise be told.

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.

2. Their object code changed (obviously), which required reanalysis of
their
object-code branch coverage.

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

What safety-critical system did you develop where you turned off
assertions
afer development? What standard (DO-178?) did you use for certification?

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.

> 
> Good design complemented by static typing and Design by Contract is unbeatable,
> IME.
> 
> :In a safety-critical system such
> :as
> :we build, you can't just generate a core dump, or ask the user what to
> :do next.
> :You have to generate a correct response to the assertion failure, and
> :you have
> :to do it very quickly.
> 
> Right. However, only an incorrect program will raise assertion violations at
> runtime. As you systematically identify and fix the errors causing them during
> development, you can turn assertions off with confidence when the system
> goes live. Then, any errors you may have missed will be handled by exception
> handlers in the usual way.
> 
> :Static assertion checks, of course, can be
> :detected and
> :corrected during development, which is why I like Ada's strong static
> :type checking.
> 
> I agree completely. Static typing is great but it isn't the *whole* story.
> 
> :There is a school of thought that says to add in assertions, test the
> :system, and
> :then remove/suppress the exceptions. I have seen too many cases of code
> :that works
> :with the assertions active, and then breaks (due to timing differences,
> 
> Yes, timing *is* something to be concerned about when applied to realtime
> systems. That's why I suggested not using assertions in the hard realtime
> threads of a process. BTW, software designed using DBC may actually run *faster*
> than code without it because you get to strip out all the defensive validity
> checks. You have already ascertained during development that operations are
> called in valid contexts so you don't have to check the context.

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

> 
> :or more
> :likely code generation errors) to have much confidence in this approach.
> 
> If that's a problem, you need to get your vendor to clean their act up.

Easier said than done! :)

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?

> 
> :Another consequence of using assertions is that you have to develop and
> :test the
> :assertions.
> 
> Correct. My initial reaction when I started using them was "Gee, I've got to
> do this extra work on top of writing the "real" code! However, I found I was
> spending about a third of the time integrating compared with my colleagues
> which meant I was saving time overall and producing more reliable code to boot.
> 
> :As a result, you need confidence that the benefits of the
> :assertions
> :outweigh the dilution of your test effort.
> 
> IME, they do.

However, it sounds like you're talking about a non-safety-critical
system, and
certainly not a hard real-time embedded safety-critical systems. In that
case,
I agree. For tools, simulations, etc. I would use all of the assertions
I could.

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.

> 
> :One of the advantages of
> :Ada's simpler
> :approach (at least, it seems simpler to me) to simple
> :pre/post-conditions (range
> :checks in particular) is that the cost of adding them is somewhat
> :reduced.
> 
> I disagree. It takes me about the same amount of time to specify an Ada
> subtype as it does to specify a more general assertion. Even if the general
> assertion is a function, I would more than likely need to write it anyway so
> would have expended the effort anyway.
> 
> :However,
> :in both languages, overuse of assertions may be just as bad as underuse.
> 
> It is possible to overuse them but 99% of developers err on the othger side. :)
> 
> :(As you can tell, I'm somewhat of an assertions heretic.
> 
> That's fine but have a go at using them where appropriate. I'm sure you'll
> become convinced.
> 
> :However, I will
> :say that
> :for non-real-time, non-safety-critical systems, they are outstanding. My
> :tool code
> :is lousy with them.)
> :
> :> Consequently, when we (a team of 5) recently
> :> reached the end of a 5 month long development effort of incremental coding
> :> and integration testing, the parts of the system that used contracting work
> :> flawlessly apart from problems resulting from misinterpretation of requirements.
> :
> :Most of the problems we see in formal testing are from misinterpretation
> :of
> :requirements - which is another issue I have with assertions as a magic
> :safety wand.
> 
> No use of assertions will stop you misinterpreting requirements. They're not
> a magic wand but they *will* help you remove a class of errors you would
> otherwise miss.
> 
> :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.

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