Re: Safety-critical development in Ada and Eiffel

[Karel Th�nissen <thoenissen@hello.nl>]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 1724 bytes --]


Marin David Condic, 561.796.8997, M/S 731-96 wrote:

[snip on the use of special assertions for timings]

>     It's a nice idea which, unfortunately can't be done. It's often
>     not well understood by those who are mostly used to some version
>     of workstation or pc based development why you can't test the code
>     with compiler option X then recompile you're code with options A,
>     B and C and pass it on as "production" software.

Sure, you only want to deliver as tested.

>     You might do this for some form of "informal" testing - maybe what
>     we took to calling "smoke testing". (Since all electronics works
>     on the principle of smoke - if you let the smoke out, it stops
>     working - the first test is to power it up and see if any smoke
>     comes out.) Under those conditions, you could compile any way you
>     like, find your problems, fix them and recompile for the "real"
>     tests.

Yes, smoke testing, I must remember that.
 
>     Once you start any sort of formal verification for a safety
>     critical system you cannot change any of the bits in the program
>     image without having to reverify the image. How much
>     reverification you do depends on lots of factors, but it's always
>     very expensive and you don't do it lightly.
> 
>     One other thing you want to consider is this: If the code *can*
>     run with runtime checks enabled, then you probably don't want to
>     turn it off for "production" anyway. What do you gain? The only
>     reason for turning it off is because it *can't* run with the
>     checks on.

Granted, but think of the additional weight of those assertions on board
of aircraft and spacecraft.

Groeten, Karel Th�nissen