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: 10f5bc,558f4a87046a001e
X-Google-Attributes: gid10f5bc,public
X-Google-Thread: 103376,2f77999989ddfe17,start
X-Google-Attributes: gid103376,public
From: WhiteR@CRPL.Cedar-Rapids.lib.IA.US (Robert S. White)
Subject: Re: Language choice and mission-criticality - Ada issues
Date: 1996/12/19
Message-ID: <59ados$hu4@flood.weeg.uiowa.edu>#1/1
X-Deja-AN: 204854549
distribution: world
references: <581c5j$qaq@adam.wins.uva.nl> <58hp0l$1rl@feep.rsn.hp.com>
content-type: Text/Plain; charset=US-ASCII
organization: my ISP is the Cedar Rapids Public Library
mime-version: 1.0
newsgroups: comp.software.testing,comp.lang.ada
Date: 1996-12-19T00:00:00+00:00
List-Id: <comp.lang.ada>


In article <Ew9Y2RAkLGuyEwCy@jessikat.demon.co.uk>, robin@jessikat.demon.co.uk 
says...
>
>In article <5956fp$la8@flood.weeg.uiowa.edu>, "Robert S. White"
><WhiteR@CRPL.Cedar-Rapids.lib.IA.US> writes

...snip...

>>  For a really "mission 
>>critical" type of language - choose one that really requires you to get your 
>>act together.  New banking software often use Eiffel or Ada.  Avionics
>>use Ada.  


>Who's proved the ADA compiler, runtimes, checking software, hardware etc
                  ^^^
>etc etc. Most damning of all who's proved the overall design.

  1.  Its Ada (not ADA) after Augusta Ada, the Countess of Lovelace.  The first
      computer programmer.  An English lady.

   ... the rest of my arguments/points are avionics related ...

  2.  I have not heard of "a formal proof" occurring often for really involved
      products.  Mathematical routines and functions yes.  More complex
      multitasking solutions such as Flight Management Systems, GPS's, etc. No.

  3.  Compilers, runtimes, Real Time Executives etc are subject to U.S. FAA
      DO-178B qualification requirements for use in commercial airlines.  The
      DoD Ada compiler validation suite is also helpful but not as important.

  4.  Low level unit testing (using the compiler and runtimes) does try to
      do a thorough test of all logic paths and input data at and beyond
      acceptable limits

  5.  Formal Qualification Tests are done using representative production
      (not engineering built) hardware with the black boxes given subject to
      test environments/scenarios designed to verify design requirments are
      met.
_______________________________________________________________________
Robert S. White                    -- an embedded sys software engineer
WhiteR@CRPL.Cedar-Rapids.lib.IA.US --long/cheap alternate I-net address