From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.3 required=5.0 tests=BAYES_00,INVALID_MSGID
	autolearn=no autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: 103376,7a58195927ccb785
X-Google-Attributes: gid103376,public
From: kaz@vision.crest.nt.com (Kaz Kylheku)
Subject: Re: Not intended for use in medical devices
Date: 1997/05/06
Message-ID: <5knk3g$2i5@bcrkh13.bnr.ca>#1/1
X-Deja-AN: 239767973
References: <3.0.32.19970504232023.006f5c8c@mail.4dcomm.com>
 <5kl8g4$fcb@bcrkh13.bnr.ca> <dewar.862916681@merv>
Organization: Prism Systems Inc.
Newsgroups: comp.lang.ada
Date: 1997-05-06T00:00:00+00:00
List-Id: <comp.lang.ada>


In article <dewar.862916681@merv>, Robert Dewar <dewar@merv.cs.nyu.edu> wrote:
>Kaz says
>
><<<<I agree with R. Dewar: your concerns are misplaced, and don't make a good case
>for avoiding inspections of the object code. In a safety critical system, an
>incorrect translation of a correct program could lead to death, injury or
>property damage. There is no other way to catch this sort of error except to
>compile the code and then inspect the results of the translation.>>
>
>  I certainly agree with this. In fact I never heard of a people using a
>  process for generating safety-critical code that did not require this
>  kind of review, and certainly the formal standards require this.
>
><<In some ways, this could make somewhat of a case for using assembly language in
>the first place, since in the process of reviewing object code, you have to
>acquire an understanding of the program at the machine language level anyway.
>I can at least appreciate where this extreme viewpoint is coming from.>>
>
>  I strongly disagree with this, and find it surprising that anyone would
>  suggest this. The review of the object code is just one of many aspects
>  of the total methodology required for safety critical code. Another
>  important aspect is more emphasis on the use of formal methods in
>  developing and analyzing the code at a high level, and these are
>  very much language dependent, and make assembly language quite useless.

I see that now. I've been thinking about this problem a lot to try to see the
object code review in its proper perspective. The scope should be verifying the
translation against the higher level specification (the Ada source program) and
only against that specification. One would not, e.g., criticize the programmer
intent in an object code review.

The higher level specification is separately tested for correctness at a
different level of abstraction, of course.  If you develop in assembly
language, then you only have one level of specification, and the object code
review has a *much* more difficult scope.

Also here is another little thought that I had: in a safety critical system, 
one way to deal with the safety issues is to identify the hazards and then
work backwards to identify scenarios in the software that could lead to the
hazards. Clearly, not every module of the code will necessarily lead to a
hazard if it contains a defect. So the object code review doesn't have to give
equal weight to weight to every instruction sequence, but should perhaps
pay extra attention to the critical code that can create a hazard.