comp.lang.ada
 help / color / mirror / Atom feed
From: Ken Garlington <GarlingtonKE@lmtas.lmco.com>
Subject: Re: Not intended for use in medical devices
Date: 1997/05/12
Date: 1997-05-12T00:00:00+00:00	[thread overview]
Message-ID: <33775001.4B3B@lmtas.lmco.com> (raw)
In-Reply-To: dewar.862916681@merv


One comment on Dr. Dewar's discussion on object code analysis (with
which I agree): A good part of the object code analysis can (and
should be) _automated_ with appropriate tools. In particular, it
is gratifying to see that some Ada compiler vendors are starting to
include object code coverage testing tools in their products. I
would like to think that the inclusion of Annex H has helped to
promote the development of such tools in the Ada community for
safety-critical systems.

Robert Dewar 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.
> 
>   The object code review is oriented to making sure that the code reflects
>   the high level intent correctly, and the objectives used in analyzing
>   this code are directly derived from the original high level code. This
>   is why Annex H in the RM requires Ada compilers to provide assistance
>   in correlating the object output to the source (see annex H if you have
>   not read it!)
> 
> How many of Ada's advantages over something like C are still relevant when you
> have to inspect the object code instruction by instruction?
> 
>   All of them, and in fact they are probably more relevant than in other
>   domains. Eliminating all possibilities of error from a program is
>   achieved by a layered approach, and the help that an Ada compiler
>   gives in smoking out typing errors etc, and the help that the high
>   level Ada semantics give in forumulating appropriate conditions for
>   verification etc are of *especially* important value in SC systems.
> 
>   Also, see annex H which is oriented towards requiring that Ada tools
>   have suitable facilities. For example, a validated C compiler may not
>   even have a capability at all for examining the generated assembly code.
>   But a 100% conforming Ada compiler (including conformance to Annex H)
>   MUST have such a capability. For example, the -S and -g switches in
>   GNAT that generate assembly language annotated with source line and
>   label information is not just a nice-to-have feature in the context
>   of annex H, it is a *required* feature.

--
LMTAS - The Fighter Enterprise - "Our Brand Means Quality"
For job listings, other info: http://www.lmtas.com or
http://www.lmco.com




  parent reply	other threads:[~1997-05-12  0:00 UTC|newest]

Thread overview: 13+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
1997-05-04  0:00 Not intended for use in medical devices Robert C. Leif, Ph.D.
1997-05-05  0:00 ` Kaz Kylheku
1997-05-06  0:00   ` Robert Dewar
1997-05-06  0:00     ` Kaz Kylheku
1997-05-12  0:00     ` Ken Garlington [this message]
1997-05-06  0:00 ` Michael F Brenner
1997-05-06  0:00   ` Kaz Kylheku
1997-05-07  0:00   ` Robert Dewar
1997-05-08  0:00     ` Matthew Heaney
1997-05-10  0:00       ` Robert Dewar
1997-05-14  0:00         ` Richard Kenner
  -- strict thread matches above, loose matches on Subject: below --
1997-05-03  0:00 Robert C. Leif, Ph.D.
1997-05-03  0:00 ` Robert Dewar
replies disabled

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox