comp.lang.ada
 help / color / mirror / Atom feed
From: sgb@erlang.praxis.co.uk (Stephen Bull)
Cc: pna, denton, gavin
Subject: Re: C++ Should not be used for Medical Devices
Date: 1997/01/27
Date: 1997-01-27T00:00:00+00:00	[thread overview]
Message-ID: <ytcg1zn5jyn.fsf@erlang.praxis.co.uk> (raw)
In-Reply-To: 3.0.32.19970119225145.006fce98@mail.4dcomm.com


Jim Chelini <jchelini@east.thomsoft.com> writes:

>  When it comes to safety critical software, I would certainly agree with
>  the use of Ada. However, I would avoid a number of features including
>  tasking and dynamic allocation. In the cases where a life is at risk
>  whether it is a medical device, aircraft, or a rail system, stick 
>  to deterministic constructs.  Once the program has completed elaboration,
>  it should not perform dynamic operations.  Also, make sure the run-time
>  is developed, documented, and TESTED to the same degree as the
>  application.  If you don't, you have left a very large hole in the
>  system.
>
>  This limits some of the more interesting features of the language
>  but the goal is to develop a safe system.

SPARK is designed to support the development of software used in
applications where correct operation is vital. Examples include avionic
and air traffic systems, railway signalling, nuclear protection systems
and medical equipment. 

The SPARK Language is a secure subset of Ada, augmented by annotations.
SPARK is formally defined and SPARK programs are predictable and can
be rigorously analysed. With its support tool, the SPARK Examiner,
and the high quality mainstream Ada products, SPARK provides a solid
engineering basis for all complex computer based systems. 

The SPARK Examiner checks the conformance of a program to the rules of
SPARK, carries out a flow analysis of the code, and supports formal
verification. Absence of run-time errors can be demonstrated rigorously. 

SPARK is a product of Praxis, a Software Engineering firm specialising
in complex systems in a variety of markets.

For further information please contact:

Denton Clutterbuck
Praxis Critical Systems
20 Manvers Street
Bath
BA1 1PX
UK

email: sparkinfo@praxis.co.uk 
tel:   +44 (0)1225 444700
fax:   +44 (0)1225 465205 

or visit our web pages:

http://www.praxis.co.uk/technols/spark/spark.htm
http://www.praxis.co.uk/services/critsys/critsys.htm

-- 
-----------------------------------------------------------------------------
 Stephen Bull  Praxis Critical Systems  20 Manvers Street  BATH  BA1 1PX  UK
    +1225 444700 (switchboard)  +1225 739286 (direct)  +1225 739281 (fax)
-----------------------------------------------------------------------------
-- 
-----------------------------------------------------------------------------
 Stephen Bull  Praxis Critical Systems  20 Manvers Street  BATH  BA1 1PX  UK
    +1225 444700 (switchboard)  +1225 739286 (direct)  +1225 739281 (fax)
-----------------------------------------------------------------------------




  parent reply	other threads:[~1997-01-27  0:00 UTC|newest]

Thread overview: 9+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
1997-01-19  0:00 C++ Should not be used for Medical Devices Dr. Robert Leif
1997-01-20  0:00 ` David C. Hoos, Sr.
1997-01-20  0:00   ` Ted Dennison
1997-01-23  0:00   ` Jim Chelini
1997-01-27  0:00 ` Stephen Bull [this message]
  -- strict thread matches above, loose matches on Subject: below --
1997-01-25  0:00 Dr. Robert Leif
1997-01-26  0:00 ` Matthew Heaney
1997-01-26  0:00 ` Robert Dewar
1997-01-27  0:00 Dr. Robert Leif
replies disabled

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