2. The High Integrity Philosophy

GNAT Pro Safety-Critical and GNAT Pro High-Security are intended to reduce costs and risks in meeting software safety or security certification standards for applications written in Ada.

One way this goal is met is through the use of language profiles: either one of the High-Integrity profiles supplied with the product, or an appropriately constrained Ada subset selected by the programmer. This will restrict Ada construct usage so that either no run-time library, or else a simple certifiable library, is used by a conforming application. In the first case (the Zero Footprint Profile) there is no need to certify any object code outside of the application code. Note that there still are some run-time source files, which provide definitions used by the compiler, but these files do not generate any object code. Depending on the certification protocol, it may still be necessary to include tests for correct access to these definitions in these run-time files.

In the second case (simple certifiable library, either for a predefined High-Integrity profile or for a user-defined configuration), the library is designed to expedite the certification process for an application that needs to use its features (e.g. concurrency, exception propagation...) For example, it may be simpler and less expensive to certify a concurrent program built on the Ravenscar Profile than to certify a sequential program with no run-time library (should concurrency need to be simulated in application code).

Although limited in terms of dynamic Ada semantics, all High-Integrity profiles fully support static Ada constructs such as private types, generic templates, and child units. Some dynamic semantics are also supported. For example, these profiles allow the use of tagged types (at library level) and other Object-Oriented Programming features, including dynamic dispatching. Note that you can prohibit the general use of dynamic dispatching at the application level using pragma Restrictions.

In addition to the High-Integrity Profiles, GNAT Pro Safety-Critical and GNAT Pro High-Security may also support a Full-Runtime Profile thus allowing usage of the complete Ada language. However, the availability of this profile is target dependent, and certification materials for the full run-time profile are not available.

A traditional problem with predefined profiles is their inflexibility: if you need to use a feature that is outside a given profile, then it is your responsibility to address the certification issues deriving from its use. GNAT Pro Safety-Critical and GNAT Pro High-Security accommodate this need by allowing you to define a profile for the specific set of features you will use. Typically this will be for features with run-time libraries that require associated certification materials. Thus your program will have a tailored run-time library supporting only those features that you have specified. Indeed, the High-Integrity profiles themselves are implemented in this manner, using the product’s run-time configurability mechanism.