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=0.6 required=5.0 tests=BAYES_20,INVALID_MSGID autolearn=no autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,bc9bd88290383e6f X-Google-Attributes: gid103376,public From: sgb@erlang.praxis.co.uk (Stephen Bull) Subject: Re: C++ Should not be used for Medical Devices Date: 1997/01/27 Message-ID: #1/1 X-Deja-AN: 212627265 sender: sgb@praxis.co.uk references: <3.0.32.19970119225145.006fce98@mail.4dcomm.com> cc: pna, denton, gavin organization: Praxis plc newsgroups: comp.lang.ada Date: 1997-01-27T00:00:00+00:00 List-Id: Jim Chelini 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) -----------------------------------------------------------------------------