Safety Critical Systems and Ada 95

Safety Critical Systems and Ada 95

[John J Cupak Jr, CCP]

[-- Attachment #1: Type: text/plain, Size: 636 bytes --]

I know Ada 95 has a Safety Annex, but has anyone actually used
it to implement a real (or even example) system?

Are there any specific reports or papers on the Safety features
of Ada 95 (other than RM95 or the Rationale)?

Inquiring minds want to know!

-- 
--------------------------------------------------------------
-                 John J. Cupak Jr, CCP                      -
- Raytheon Systems Company - Software Engineering Laboratory -
- tel: 978-858-1222   email (work): jcj@swl.msd.ray.com      -
- fax: 978-858-4336   email (home): jcupak@aol.com           -
--------------------------------------------------------------

[-- Attachment #2: Card for Cupak Jr, CCP, John J. --]
[-- Type: text/x-vcard, Size: 481 bytes --]

begin:          vcard
fn:             John J. Cupak Jr, CCP
n:              Cupak Jr, CCP;John J.
org:            TWK
adr;dom:        50 Apple Hill Road;;MS T3MN35;Tewksbury;MA;01879;
email;internet: jcj@swl.msd.ray.com
title:          Senior Software Engineer / Instructor
tel;work:       225-1222
tel;fax:        978-858-4336
tel;home:       603-595-8240
note:           EMAIL;AOL:jcupak@aol.com
x-mozilla-cpt:  ;0
x-mozilla-html: TRUE
version:        2.1
end:            vcard

Re: Safety Critical Systems and Ada 95

[JP Thornley]

In article: <357EB552.5CF3EB9@swl.msd.ray.com>  "John J Cupak Jr, CCP" 
<jcj@swl.msd.ray.com> writes:
> 
> I know Ada 95 has a Safety Annex, but has anyone actually used
> it to implement a real (or even example) system?
> 
> Are there any specific reports or papers on the Safety features
> of Ada 95 (other than RM95 or the Rationale)?
> 
> Inquiring minds want to know!
> 

There are (AFAIK) no compilers that implement Annex H (but there are no 
tests for conformance either!).

[But I've just remembered that GNAT claims to implement 100% of the 
language - must see what they do for the Annex H pragmas.]

It's important to realise that pragma Restrictions does not *impose* 
that restriction on the code. ARM 13.12 says "A pragma Restrictions 
expresses the user's intent to abide by certain restrictions." and if 
the user breaks the restriction the program need not do anything about 
it. [In fact I think the program becomes erroneous - which isn't really 
very useful.]

Probably of more use is the Technical Report currently being written by 
the Annex H Rapporteur Group (the HRG - a subgroup of WG9). This is 
titled (something like) "Guidance on the use of the Ada language for 
high-integrity software" and a preliminary draft has recently been 
circulated within the HRG mailing list for comment. There is another 
meeting of the Group in a couple of weeks to review comments received 
and I think the plan is that the draft resulting from that meeting is to 
be published in Ada Letters later this year. [Once the report is 
formally circulated within ISO then I believe that copyright 
restrictions will prevent it being published elsewhere.]

This report has very little to say about Annex H, but concentrates on 
the links between the features of the language and how the various 
verification and validation techniques are affected by their use.

The other excellent reference in this area is John Barnes' book: High 
Integrity Ada, The SPARK Approach, but that makes no reference to
Annex H at all.

Phil Thornley

-- 
------------------------------------------------------------------------
| JP Thornley    EMail jpt@diphi.demon.co.uk                           |
|                      phil.thornley@acm.org                           |
------------------------------------------------------------------------

Re: Safety Critical Systems and Ada 95

[Tucker Taft]

JP Thornley (jpt@diphi.demon.co.uk) wrote:

: ...
: It's important to realise that pragma Restrictions does not *impose* 
: that restriction on the code. ARM 13.12 says "A pragma Restrictions 
: expresses the user's intent to abide by certain restrictions." and if 
: the user breaks the restriction the program need not do anything about 
: it. [In fact I think the program becomes erroneous - which isn't really 
: very useful.]

Not quite.  

Any restriction whose violation can be detected at compile-time
or link-time is treated as an error by the compiler.  It is only
restrictions that are undetectable prior to run-time that can
result in erroneous execution upon violation.

This rule is indicated by RM 13.12(8) which says 

  ... a partition shall obey the restriction ...

The word "shall" here means that the compiler or the
linker is required to detect violation of the restriction.

Different rules may apply to particular restrictions, but
13.12(8) specifies the default rule.

: ...
: Phil Thornley
: | JP Thornley    EMail jpt@diphi.demon.co.uk                           |
: |                      phil.thornley@acm.org                           |

--
-Tucker Taft   stt@inmet.com   http://www.inmet.com/~stt/
Intermetrics, Inc.  Burlington, MA  USA

Re: Safety Critical Systems and Ada 95

[Robert I. Eachus]

In article <EuEBLM.97x.0.-s@inmet.camb.inmet.com> stt@houdini.camb.inmet.com (Tucker Taft) writes:

  > Any restriction whose violation can be detected at compile-time
  > or link-time is treated as an error by the compiler.  It is only
  > restrictions that are undetectable prior to run-time that can
  > result in erroneous execution upon violation.

   I'd like to amplify a bit.  What Tuck says is correct, but
mysterious to people who don't have the full context.  There are
several restrictions which are of great use in a safety context, and
are also useful for performance tuning.  Ada 95 combines these into a
single pragma, even though it is not always possible to detect
violations at compile time.  The easiest example to understand is

     pragma Restrictions(Max_Tasks => 0);

   Annex D requires support of the identifier, but for say Max_Tasks
=> 100, it is impossible to tell whether some programs violate the
restriction at compile time.  However, Annex H at H.4(2) requires that
Max_Tasks of zero be checked at compile or link time.  ("checked prior to
program execution.")

   So pragma Restrictions with some arguments will not be useful for
Annex H purposes.  But the restrictions defined in Annex H can and, if
Annex H is supported, must be checked prior to execution. There are
technically three exceptions: No_Exceptions and hardware signaled
exceptions, No_Recursion, and recursion which can not be detected at
compile time, and No_Reentrancy in a program with multiple tasks.  The
obvious way to avoid those problems is to choose a sensible set of
restrictions.  For example, No_Access_Subprograms and No_Dispatch
should be used with No_Recursion so that all potentially recursive
calls can be checked at compile time, and you can use modular types to
avoid cases where the hardware would signal integer overflow.
--

					Robert I. Eachus

with Standard_Disclaimer;
use  Standard_Disclaimer;
function Message (Text: in Clever_Ideas) return Better_Ideas is...

Re: Safety Critical Systems and Ada 95

[Rakesh Malhotra]

John J Cupak Jr, CCP wrote:
> 
> I know Ada 95 has a Safety Annex, but has anyone actually used
> it to implement a real (or even example) system?
> 
> Are there any specific reports or papers on the Safety features
> of Ada 95 (other than RM95 or the Rationale)?
> 
Have not used the Annex.  I do not know of papers that deal specifically
with safety and the Ada95 annex H however regarding the safety features
of Ada in general, there are quite a few available documents: 

1. There is a toolset called SPARK (from Praxis Critical Systems in the
UK) that implements/enforces a safety critical sub-set of Ada83/95 and
analyses Ada programs for correctness (the tool does much more than just
enforce a subset, though).   SPARK documentation talks about Ada
subsets.

2. There is a book called High Integrity Ada by John Barnes that
discusses the SPARK approach further.

3. Developing Safety Systems by IC Pyle talks about use of Ada (though
it deals only with Ada83).

4. Safer C by Les Hatton discusses use of C in safety critical systems
and contains a comparision with Ada.

5. Aonix have a Safety Critical Systems development handbook you can
order.   There are also a couple of papers that people at Aonix have
published as a rejoinder to Safer C.  You may be able to find these at
Aonix's web site or request for them.

6. Couple of international standards including RIA 23, CENELEC discuss
software development techniques including choice of programming
languages for safety critical systems.  Most of these standards have
sections discussing C, Ada, assembly etc.

Hope this helps.
--
Rakesh

Re: Safety Critical Systems and Ada 95

[Brian Rogoff]

On Wed, 10 Jun 1998, Rakesh Malhotra wrote:
> John J Cupak Jr, CCP wrote:
> > 
> > I know Ada 95 has a Safety Annex, but has anyone actually used
> > it to implement a real (or even example) system?
> > 
> > Are there any specific reports or papers on the Safety features
> > of Ada 95 (other than RM95 or the Rationale)?
> > 
> Have not used the Annex.  I do not know of papers that deal specifically
> with safety and the Ada95 annex H however regarding the safety features
> of Ada in general, there are quite a few available documents: 
> 
> ... snip ...

In the May 13 issue of "Electronic Design", the EDA watch section is about
the use of Ada 95 as a hardware/software codesign language, and has some
discussion of Annex H and a subset based on intersecting with the VHDL
reserved word set. While some of the details sounded goofy to me, I think
the general idea is quite good. There is a lot of talk about Java as such 
a language, but Ada is clearly better.

-- Brian

Re: Safety Critical Systems and Ada 95

[Rakesh Malhotra]

John J Cupak Jr, CCP wrote:
> 
> I know Ada 95 has a Safety Annex, but has anyone actually used
> it to implement a real (or even example) system?
> 
> Are there any specific reports or papers on the Safety features
> of Ada 95 (other than RM95 or the Rationale)?
> 
Have not used the Annex.  I do not know of papers that deal specifically
with safety and the Ada95 annex H however regarding the safety features
of Ada in general, there are quite a few available documents: 

1. There is a toolset called SPARK (from Praxis Critical Systems in the
UK) that implements/enforces a safety critical sub-set of Ada83/95 and
analyses Ada programs for correctness (the tool does much more than just
enforce a subset, though).   SPARK documentation talks about Ada
subsets.

2. There is a book called High Integrity Ada by John Barnes that
discusses the SPARK approach further.

3. Developing Safety Systems by IC Pyle talks about use of Ada (though
it deals only with Ada83).

4. Safer C by Les Hatton discusses use of C in safety critical systems
and contains a comparision with Ada.

5. Aonix have a Safety Critical Systems development handbook you can
order.   There are also a couple of papers that people at Aonix have
published as a rejoinder to Safer C.  You may be able to find these at
Aonix's web site or request for them.

6. Couple of international standards including RIA 23, CENELEC discuss
software development techniques including choice of programming
languages for safety critical systems.  Most of these standards have
sections discussing C, Ada, assembly etc.

Hope this helps.
--
Rakesh

Re: Safety Critical Systems and Ada 95

[Rakesh Malhotra]

John J Cupak Jr, CCP wrote:
> 
> I know Ada 95 has a Safety Annex, but has anyone actually used
> it to implement a real (or even example) system?
> 
> Are there any specific reports or papers on the Safety features
> of Ada 95 (other than RM95 or the Rationale)?
> 
Have not used the Annex.  I do not know of papers that deal specifically
with safety and the Ada95 annex H however regarding the safety features
of Ada in general, there are quite a few available documents: 

1. There is a toolset called SPARK (from Praxis Critical Systems in the
UK) that implements/enforces a safety critical sub-set of Ada83/95 and
analyses Ada programs for correctness (the tool does much more than just
enforce a subset, though).   SPARK documentation talks about Ada
subsets.

2. There is a book called High Integrity Ada by John Barnes that
discusses the SPARK approach further.

3. Developing Safety Systems by IC Pyle talks about use of Ada (though
it deals only with Ada83).

4. Safer C by Les Hatton discusses use of C in safety critical systems
and contains a comparision with Ada.

5. Aonix have a Safety Critical Systems development handbook you can
order.   There are also a couple of papers that people at Aonix have
published as a rejoinder to Safer C.  You may be able to find these at
Aonix's web site or request for them.

6. Couple of international standards including RIA 23, CENELEC discuss
software development techniques including choice of programming
languages for safety critical systems.  Most of these standards have
sections discussing C, Ada, assembly etc.

Hope this helps.
--
Rakesh

Re: Safety Critical Systems and Ada 95

[Rakesh Malhotra]

John J Cupak Jr, CCP wrote:
> 
> I know Ada 95 has a Safety Annex, but has anyone actually used
> it to implement a real (or even example) system?
> 
> Are there any specific reports or papers on the Safety features
> of Ada 95 (other than RM95 or the Rationale)?
> 
Have not used the Annex.  I do not know of papers that deal specifically
with safety and the Ada95 annex H however regarding the safety features
of Ada in general, there are quite a few available documents: 

1. There is a toolset called SPARK (from Praxis Critical Systems in the
UK) that implements/enforces a safety critical sub-set of Ada83/95 and
analyses Ada programs for correctness (the tool does much more than just
enforce a subset, though).   SPARK documentation talks about Ada
subsets.

2. There is a book called High Integrity Ada by John Barnes that
discusses the SPARK approach further.

3. Developing Safety Systems by IC Pyle talks about use of Ada (though
it deals only with Ada83).

4. Safer C by Les Hatton discusses use of C in safety critical systems
and contains a comparision with Ada.

5. Aonix have a Safety Critical Systems development handbook you can
order.   There are also a couple of papers that people at Aonix have
published as a rejoinder to Safer C.  You may be able to find these at
Aonix's web site or request for them.

6. Couple of international standards including RIA 23, CENELEC discuss
software development techniques including choice of programming
languages for safety critical systems.  Most of these standards have
sections discussing C, Ada, assembly etc.

Hope this helps.
--
Rakesh